let X be set ; :: thesis: inf X c= sup X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in inf X or x in sup X )
assume A1: x in inf X ; :: thesis: x in sup X
consider y being Element of On X;
reconsider y = y as Ordinal by A1, ORDINAL1:def 10, SETFAM_1:2;
On X c= sup X by Def7;
then y in sup X by A1, SETFAM_1:2, TARSKI:def 3;
then ( y c= sup X & x in y ) by A1, ORDINAL1:def 2, SETFAM_1:2, SETFAM_1:def 1;
hence x in sup X ; :: thesis: verum