per cases ( A " {x} = {} or A " {x} <> {} ) ;
suppose A " {x} = {} ; :: thesis: A <- x is natural
hence A <- x is natural by SETFAM_1:def 1; :: thesis: verum
end;
suppose A " {x} <> {} ; :: thesis: A <- x is natural
then consider y being object such that
A1: y in A " {x} by XBOOLE_0:def 1;
A2: A " {x} c= dom A by RELAT_1:132;
then y in dom A by A1;
then reconsider y = y as Element of NAT ;
A3: A <- x is Ordinal by A2, XBOOLE_1:1, ORDINAL3:11;
A <- x c= y by A1, SETFAM_1:3;
hence A <- x is natural by A3; :: thesis: verum
end;
end;