let A be Ordinal; :: thesis: for X being set st A in X holds
A in sup X
let X be set ; :: thesis: ( A in X implies A in sup X )
assume A in X ; :: thesis: A in sup X
then ( A in On X & On X c= sup X ) by Def7, ORDINAL1:def 10;
hence A in sup X ; :: thesis: verum