Theorem isGreatest_pair

Modification history