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