let A be Ordinal; :: thesis: for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
let X, Y be set ; :: thesis: ( A in X & X c= Y implies inf Y c= inf X )
assume A in X ; :: thesis: ( not X c= Y or inf Y c= inf X )
then A1: On X <> 0 by ORDINAL1:def 9;
assume X c= Y ; :: thesis: inf Y c= inf X
then On X c= On Y by Th9;
hence inf Y c= inf X by A1, SETFAM_1:6; :: thesis: verum