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 <> {} by ORDINAL1:def 10;
assume X c= Y ; :: thesis: inf Y c= inf X
then On X c= On Y by Th11;
hence inf Y c= inf X by A1, SETFAM_1:7; :: thesis: verum