Theorem Set.Finite.iSup_biInf_of_antitone

Modification history