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 A1: A in On X by ORDINAL1:def 9;
On X c= sup X by Def3;
hence A in sup X by A1; :: thesis: verum