let A be Ordinal; :: thesis: for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
let X be set ; :: thesis: ( A in sup X implies ex B being Ordinal st
( B in X & A c= B ) )
assume that
A1: A in sup X and
A2: for B being Ordinal st B in X holds
not A c= B ; :: thesis: contradiction
for B being Ordinal st B in X holds
B in A by A2, ORDINAL1:16;
then sup X c= A by Th20;
hence contradiction by A1, ORDINAL1:5; :: thesis: verum