set F1 = { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } ;
set F2 = { [k,1] where k is Element of omega : verum } ;
{ [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } c= [:NAT,NAT:]

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } or o in [:NAT,NAT:] )
assume o in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } ; :: thesis: o in [:NAT,NAT:]
then ex i, j being Element of omega st
( o = [i,j] & i,j are_coprime & j <> {} ) ;
hence o in [:NAT,NAT:] ; :: thesis: verum

end;

then { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } c= [:NAT,NAT:] ;
then A1: RAT+ c= [:NAT,NAT:] \/ NAT by XBOOLE_1:13;
then A2: RAT+ \/ DEDEKIND_CUTS c= ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS by XBOOLE_1:9;
A3: bool RAT+ c= bool ([:NAT,NAT:] \/ NAT) by A1, ZFMISC_1:67;
A4: REAL+ c= ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS by A2;
A5: ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS c= ([:NAT,NAT:] \/ NAT) \/ (bool RAT+) by XBOOLE_1:9;
([:NAT,NAT:] \/ NAT) \/ (bool RAT+) c= (([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)) \/ (bool ([:NAT,NAT:] \/ NAT)) by A3, XBOOLE_1:9;
then A6: REAL+ c= (([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)) \/ (bool ([:NAT,NAT:] \/ NAT)) by A4, A5;
then [:NAT,REAL+:] c= [:NAT,((([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)) \/ (bool ([:NAT,NAT:] \/ NAT))):] by ZFMISC_1:96;
then A7: REAL+ \/ [:NAT,REAL+:] c= ((([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)) \/ (bool ([:NAT,NAT:] \/ NAT))) \/ [:NAT,((([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)) \/ (bool ([:NAT,NAT:] \/ NAT))):] by A6, XBOOLE_1:13;
set N1 = [:NAT,NAT:] \/ NAT;
set N2 = ([:NAT,NAT:] \/ NAT) \/ (bool ([:NAT,NAT:] \/ NAT));
[:{0},REAL+:] c= [:NAT,REAL+:] by ZFMISC_1:96;
then REAL+ \/ [:{0},REAL+:] c= REAL+ \/ [:NAT,REAL+:] by XBOOLE_1:9;
hence for N1, N2 being set st N1 = [:NAT,NAT:] \/ NAT & N2 = N1 \/ (bool N1) holds
REAL c= N2 \/ [:NAT,N2:] by A7; :: thesis: verum