let A be Ordinal; :: thesis: for X being set st A in X holds
inf X c= A
let X be set ; :: thesis: ( A in X implies inf X c= A )
assume A in X ; :: thesis: inf X c= A
then A in On X by ORDINAL1:def 9;
hence inf X c= A by SETFAM_1:3; :: thesis: verum