let A be Ordinal; :: thesis: for X being set st X c= A holds
meet X is Ordinal
let X be set ; :: thesis: ( X c= A implies meet X is Ordinal )
assume X c= A ; :: thesis: meet X is Ordinal
then inf X = meet X by Th6;
hence meet X is Ordinal ; :: thesis: verum