let A be set ; :: thesis: ( A is Subset of REAL? & not REAL in A iff ( A is Subset of R^1 & NAT /\ A = {} ) )

thus ( A is Subset of REAL? & not REAL in A implies ( A is Subset of R^1 & NAT /\ A = {} ) ) :: thesis: ( A is Subset of R^1 & NAT /\ A = {} implies ( A is Subset of REAL? & not REAL in A ) )

A8: A is Subset of R^1 and

A9: NAT /\ A = {} ; :: thesis: ( A is Subset of REAL? & not REAL in A )

A10: A c= REAL \ NAT

then A c= (REAL \ NAT) \/ {REAL} by A10;

hence A is Subset of REAL? by Def8; :: thesis: not REAL in A

thus not REAL in A :: thesis: verum

thus ( A is Subset of REAL? & not REAL in A implies ( A is Subset of R^1 & NAT /\ A = {} ) ) :: thesis: ( A is Subset of R^1 & NAT /\ A = {} implies ( A is Subset of REAL? & not REAL in A ) )

proof

assume that
assume that

A1: A is Subset of REAL? and

A2: not REAL in A ; :: thesis: ( A is Subset of R^1 & NAT /\ A = {} )

A c= the carrier of REAL? by A1;

then A3: A c= (REAL \ NAT) \/ {REAL} by Def8;

A c= REAL

thus NAT /\ A = {} :: thesis: verum

end;A1: A is Subset of REAL? and

A2: not REAL in A ; :: thesis: ( A is Subset of R^1 & NAT /\ A = {} )

A c= the carrier of REAL? by A1;

then A3: A c= (REAL \ NAT) \/ {REAL} by Def8;

A c= REAL

proof

hence
A is Subset of R^1
by TOPMETR:17; :: thesis: NAT /\ A = {}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in REAL )

assume A4: x in A ; :: thesis: x in REAL

then ( x in REAL \ NAT or x in {REAL} ) by A3, XBOOLE_0:def 3;

hence x in REAL by A2, A4, TARSKI:def 1; :: thesis: verum

end;assume A4: x in A ; :: thesis: x in REAL

then ( x in REAL \ NAT or x in {REAL} ) by A3, XBOOLE_0:def 3;

hence x in REAL by A2, A4, TARSKI:def 1; :: thesis: verum

thus NAT /\ A = {} :: thesis: verum

proof

set x = the Element of NAT /\ A;

assume A5: NAT /\ A <> {} ; :: thesis: contradiction

then A6: the Element of NAT /\ A in NAT by XBOOLE_0:def 4;

A7: the Element of NAT /\ A in A by A5, XBOOLE_0:def 4;

end;assume A5: NAT /\ A <> {} ; :: thesis: contradiction

then A6: the Element of NAT /\ A in NAT by XBOOLE_0:def 4;

A7: the Element of NAT /\ A in A by A5, XBOOLE_0:def 4;

per cases
( the Element of NAT /\ A in REAL \ NAT or the Element of NAT /\ A in {REAL} )
by A3, A7, XBOOLE_0:def 3;

end;

suppose
the Element of NAT /\ A in {REAL}
; :: thesis: contradiction

then
the Element of NAT /\ A = REAL
by TARSKI:def 1;

then REAL in REAL by A6, NUMBERS:19;

hence contradiction ; :: thesis: verum

end;then REAL in REAL by A6, NUMBERS:19;

hence contradiction ; :: thesis: verum

A8: A is Subset of R^1 and

A9: NAT /\ A = {} ; :: thesis: ( A is Subset of REAL? & not REAL in A )

A10: A c= REAL \ NAT

proof

REAL \ NAT c= (REAL \ NAT) \/ {REAL}
by XBOOLE_1:7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in REAL \ NAT )

assume A11: x in A ; :: thesis: x in REAL \ NAT

then not x in NAT by A9, XBOOLE_0:def 4;

hence x in REAL \ NAT by A8, A11, TOPMETR:17, XBOOLE_0:def 5; :: thesis: verum

end;assume A11: x in A ; :: thesis: x in REAL \ NAT

then not x in NAT by A9, XBOOLE_0:def 4;

hence x in REAL \ NAT by A8, A11, TOPMETR:17, XBOOLE_0:def 5; :: thesis: verum

then A c= (REAL \ NAT) \/ {REAL} by A10;

hence A is Subset of REAL? by Def8; :: thesis: not REAL in A

thus not REAL in A :: thesis: verum

proof

assume
REAL in A
; :: thesis: contradiction

then REAL in REAL by A8, TOPMETR:17;

hence contradiction ; :: thesis: verum

end;then REAL in REAL by A8, TOPMETR:17;

hence contradiction ; :: thesis: verum