let X be set ; :: thesis: ( X is ordinal-membered iff for x being set st x in X holds
x is ordinal )
thus ( X is ordinal-membered implies for x being set st x in X holds
x is ordinal ) :: thesis: ( ( for x being set st x in X holds
x is ordinal ) implies X is ordinal-membered )

proof

assume ex a being ordinal number st X c= a ; :: according to ORDINAL6:def 1 :: thesis: for x being set st x in X holds
x is ordinal
hence for x being set st x in X holds
x is ordinal ; :: thesis: verum

end;

assume Z1: for x being set st x in X holds
x is ordinal ; :: thesis: X is ordinal-membered
take a = sup X; :: according to ORDINAL6:def 1 :: thesis: X c= a
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in a )
assume Z2: x in X ; :: thesis: x in a
then x is Ordinal by Z1;
hence x in a by Z2, ORDINAL2:19; :: thesis: verum