let X be set ; :: thesis: ( X is ordinal-membered iff On X = X )

hereby :: thesis: ( On X = X implies X is ordinal-membered )

assume A1: X is ordinal-membered ; :: thesis: On X = X
thus On X = X :: thesis: verum

proof

thus On X c= X by ORDINAL2:7; :: according to XBOOLE_0:def 10 :: thesis: X c= On X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in On X )
thus ( not x in X or x in On X ) by A1, ORDINAL1:def 9; :: thesis: verum

end;

end;

thus ( On X = X implies X is ordinal-membered ) ; :: thesis: verum