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