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 A1: ( A in sup X & ( for B being Ordinal st B in X holds
not A c= B ) ) ; :: thesis: contradiction
then for B being Ordinal st B in X holds
B in A by ORDINAL1:26;
then sup X c= A by Th28;
hence contradiction by A1, ORDINAL1:7; :: thesis: verum