set L = real-anti-diagonal ;

set S2 = Sorgenfrey-plane ;

reconsider C = [:RAT,RAT:] as dense Subset of Sorgenfrey-plane by Th2;

defpred S_{1}[ object , object ] means ex S being set ex U, V being open Subset of Sorgenfrey-plane st

( $1 = S & $2 = U /\ C & S c= U & real-anti-diagonal \ S c= V & U misses V );

A1: exp (2,omega) in exp (2,(exp (2,omega))) by CARD_5:14;

card C c= omega by CARD_3:def 14, CARD_4:7;

then A2: exp (2,(card C)) c= exp (2,omega) by CARD_2:93;

assume A3: for W, V being Subset of Sorgenfrey-plane st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of Sorgenfrey-plane st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; :: according to COMPTS_1:def 3 :: thesis: contradiction

A4: for a being object st a in bool real-anti-diagonal holds

ex b being object st S_{1}[a,b]

A14: dom G = bool real-anti-diagonal and

A15: for a being object st a in bool real-anti-diagonal holds

S_{1}[a,G . a]
from CLASSES1:sch 1(A4);

G is one-to-one

rng G c= bool C

then card (bool real-anti-diagonal) c= card (bool C) by A33, A14, XBOOLE_1:1;

then A36: exp (2,continuum) c= card (bool C) by CARD_2:31, Th3;

card (bool C) = exp (2,(card C)) by CARD_2:31;

then exp (2,continuum) c= exp (2,omega) by A36, A2, XBOOLE_1:1;

then exp (2,omega) in exp (2,omega) by A1, TOPGEN_3:29;

hence contradiction ; :: thesis: verum

set S2 = Sorgenfrey-plane ;

reconsider C = [:RAT,RAT:] as dense Subset of Sorgenfrey-plane by Th2;

defpred S

( $1 = S & $2 = U /\ C & S c= U & real-anti-diagonal \ S c= V & U misses V );

A1: exp (2,omega) in exp (2,(exp (2,omega))) by CARD_5:14;

card C c= omega by CARD_3:def 14, CARD_4:7;

then A2: exp (2,(card C)) c= exp (2,omega) by CARD_2:93;

assume A3: for W, V being Subset of Sorgenfrey-plane st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of Sorgenfrey-plane st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; :: according to COMPTS_1:def 3 :: thesis: contradiction

A4: for a being object st a in bool real-anti-diagonal holds

ex b being object st S

proof

consider G being Function such that
let a be object ; :: thesis: ( a in bool real-anti-diagonal implies ex b being object st S_{1}[a,b] )

assume a in bool real-anti-diagonal ; :: thesis: ex b being object st S_{1}[a,b]

then reconsider aa = a as Subset of real-anti-diagonal ;

reconsider a9 = real-anti-diagonal \ aa as Subset of real-anti-diagonal by XBOOLE_1:36;

reconsider A = aa, B = a9 as closed Subset of Sorgenfrey-plane by Th6;

end;assume a in bool real-anti-diagonal ; :: thesis: ex b being object st S

then reconsider aa = a as Subset of real-anti-diagonal ;

reconsider a9 = real-anti-diagonal \ aa as Subset of real-anti-diagonal by XBOOLE_1:36;

reconsider A = aa, B = a9 as closed Subset of Sorgenfrey-plane by Th6;

per cases
( a = {} or a = real-anti-diagonal or ( a <> {} & a <> real-anti-diagonal ) )
;

end;

suppose A5:
a = {}
; :: thesis: ex b being object st S_{1}[a,b]

take
{}
; :: thesis: S_{1}[a, {} ]

take {} ; :: thesis: ex U, V being open Subset of Sorgenfrey-plane st

( a = {} & {} = U /\ C & {} c= U & real-anti-diagonal \ {} c= V & U misses V )

take {} Sorgenfrey-plane ; :: thesis: ex V being open Subset of Sorgenfrey-plane st

( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= V & {} Sorgenfrey-plane misses V )

take [#] Sorgenfrey-plane ; :: thesis: ( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= [#] Sorgenfrey-plane & {} Sorgenfrey-plane misses [#] Sorgenfrey-plane )

thus ( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= [#] Sorgenfrey-plane & {} Sorgenfrey-plane misses [#] Sorgenfrey-plane ) by A5, Th4, XBOOLE_1:65; :: thesis: verum

end;take {} ; :: thesis: ex U, V being open Subset of Sorgenfrey-plane st

( a = {} & {} = U /\ C & {} c= U & real-anti-diagonal \ {} c= V & U misses V )

take {} Sorgenfrey-plane ; :: thesis: ex V being open Subset of Sorgenfrey-plane st

( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= V & {} Sorgenfrey-plane misses V )

take [#] Sorgenfrey-plane ; :: thesis: ( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= [#] Sorgenfrey-plane & {} Sorgenfrey-plane misses [#] Sorgenfrey-plane )

thus ( a = {} & {} = ({} Sorgenfrey-plane) /\ C & {} c= {} Sorgenfrey-plane & real-anti-diagonal \ {} c= [#] Sorgenfrey-plane & {} Sorgenfrey-plane misses [#] Sorgenfrey-plane ) by A5, Th4, XBOOLE_1:65; :: thesis: verum

suppose A6:
a = real-anti-diagonal
; :: thesis: ex b being object st S_{1}[a,b]

take
([#] Sorgenfrey-plane) /\ C
; :: thesis: S_{1}[a,([#] Sorgenfrey-plane) /\ C]

take real-anti-diagonal ; :: thesis: ex U, V being open Subset of Sorgenfrey-plane st

( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = U /\ C & real-anti-diagonal c= U & real-anti-diagonal \ real-anti-diagonal c= V & U misses V )

take [#] Sorgenfrey-plane ; :: thesis: ex V being open Subset of Sorgenfrey-plane st

( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= V & [#] Sorgenfrey-plane misses V )

take {} Sorgenfrey-plane ; :: thesis: ( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= {} Sorgenfrey-plane & [#] Sorgenfrey-plane misses {} Sorgenfrey-plane )

thus ( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= {} Sorgenfrey-plane & [#] Sorgenfrey-plane misses {} Sorgenfrey-plane ) by A6, Th4, XBOOLE_1:37, XBOOLE_1:65; :: thesis: verum

end;take real-anti-diagonal ; :: thesis: ex U, V being open Subset of Sorgenfrey-plane st

( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = U /\ C & real-anti-diagonal c= U & real-anti-diagonal \ real-anti-diagonal c= V & U misses V )

take [#] Sorgenfrey-plane ; :: thesis: ex V being open Subset of Sorgenfrey-plane st

( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= V & [#] Sorgenfrey-plane misses V )

take {} Sorgenfrey-plane ; :: thesis: ( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= {} Sorgenfrey-plane & [#] Sorgenfrey-plane misses {} Sorgenfrey-plane )

thus ( a = real-anti-diagonal & ([#] Sorgenfrey-plane) /\ C = ([#] Sorgenfrey-plane) /\ C & real-anti-diagonal c= [#] Sorgenfrey-plane & real-anti-diagonal \ real-anti-diagonal c= {} Sorgenfrey-plane & [#] Sorgenfrey-plane misses {} Sorgenfrey-plane ) by A6, Th4, XBOOLE_1:37, XBOOLE_1:65; :: thesis: verum

suppose A7:
( a <> {} & a <> real-anti-diagonal )
; :: thesis: ex b being object st S_{1}[a,b]

(aa `) ` = a9 `
;

then A8: B <> {} real-anti-diagonal by A7;

A misses B by XBOOLE_1:79;

then consider P, Q being Subset of Sorgenfrey-plane such that

A9: P is open and

A10: Q is open and

A11: A c= P and

A12: B c= Q and

A13: P misses Q by A8, A3, A7;

take P /\ C ; :: thesis: S_{1}[a,P /\ C]

thus S_{1}[a,P /\ C]
by A9, A10, A11, A12, A13; :: thesis: verum

end;then A8: B <> {} real-anti-diagonal by A7;

A misses B by XBOOLE_1:79;

then consider P, Q being Subset of Sorgenfrey-plane such that

A9: P is open and

A10: Q is open and

A11: A c= P and

A12: B c= Q and

A13: P misses Q by A8, A3, A7;

take P /\ C ; :: thesis: S

thus S

A14: dom G = bool real-anti-diagonal and

A15: for a being object st a in bool real-anti-diagonal holds

S

G is one-to-one

proof

then A33:
card (dom G) c= card (rng G)
by CARD_1:10;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom G or not y in dom G or not G . x = G . y or x = y )

assume that

A16: x in dom G and

A17: y in dom G ; :: thesis: ( not G . x = G . y or x = y )

reconsider A = x, B = y as Subset of real-anti-diagonal by A16, A17, A14;

assume that

A18: G . x = G . y and

A19: x <> y ; :: thesis: contradiction

consider z being object such that

A20: ( ( z in A & not z in B ) or ( z in B & not z in A ) ) by A19, TARSKI:2;

A21: ( z in A \ B or z in B \ A ) by A20, XBOOLE_0:def 5;

S_{1}[B,G . B]
by A15;

then consider UB, VB being open Subset of Sorgenfrey-plane such that

A22: G . B = UB /\ C and

A23: B c= UB and

A24: real-anti-diagonal \ B c= VB and

A25: UB misses VB ;

S_{1}[A,G . A]
by A15;

then consider UA, VA being open Subset of Sorgenfrey-plane such that

A26: G . A = UA /\ C and

A27: A c= UA and

A28: real-anti-diagonal \ A c= VA and

A29: UA misses VA ;

B \ A = B /\ (A `) by SUBSET_1:13;

then A30: B \ A c= UB /\ VA by A28, A23, XBOOLE_1:27;

A \ B = A /\ (B `) by SUBSET_1:13;

then A \ B c= UA /\ VB by A27, A24, XBOOLE_1:27;

then ( ex z being object st

( z in C & z in UA /\ VB ) or ex z being object st

( z in C & z in UB /\ VA ) ) by XBOOLE_0:3, A30, A21, TOPS_1:45;

then consider z being set such that

A31: z in C and

A32: ( z in UA /\ VB or z in UB /\ VA ) ;

( ( z in UA & z in VB ) or ( z in UB & z in VA ) ) by A32, XBOOLE_0:def 4;

then ( ( z in UA & not z in UB ) or ( z in UB & not z in UA ) ) by A29, A25, XBOOLE_0:3;

then ( ( z in G . A & not z in G . B ) or ( z in G . B & not z in G . A ) ) by A26, A22, A31, XBOOLE_0:def 4;

hence contradiction by A18; :: thesis: verum

end;assume that

A16: x in dom G and

A17: y in dom G ; :: thesis: ( not G . x = G . y or x = y )

reconsider A = x, B = y as Subset of real-anti-diagonal by A16, A17, A14;

assume that

A18: G . x = G . y and

A19: x <> y ; :: thesis: contradiction

consider z being object such that

A20: ( ( z in A & not z in B ) or ( z in B & not z in A ) ) by A19, TARSKI:2;

A21: ( z in A \ B or z in B \ A ) by A20, XBOOLE_0:def 5;

S

then consider UB, VB being open Subset of Sorgenfrey-plane such that

A22: G . B = UB /\ C and

A23: B c= UB and

A24: real-anti-diagonal \ B c= VB and

A25: UB misses VB ;

S

then consider UA, VA being open Subset of Sorgenfrey-plane such that

A26: G . A = UA /\ C and

A27: A c= UA and

A28: real-anti-diagonal \ A c= VA and

A29: UA misses VA ;

B \ A = B /\ (A `) by SUBSET_1:13;

then A30: B \ A c= UB /\ VA by A28, A23, XBOOLE_1:27;

A \ B = A /\ (B `) by SUBSET_1:13;

then A \ B c= UA /\ VB by A27, A24, XBOOLE_1:27;

then ( ex z being object st

( z in C & z in UA /\ VB ) or ex z being object st

( z in C & z in UB /\ VA ) ) by XBOOLE_0:3, A30, A21, TOPS_1:45;

then consider z being set such that

A31: z in C and

A32: ( z in UA /\ VB or z in UB /\ VA ) ;

( ( z in UA & z in VB ) or ( z in UB & z in VA ) ) by A32, XBOOLE_0:def 4;

then ( ( z in UA & not z in UB ) or ( z in UB & not z in UA ) ) by A29, A25, XBOOLE_0:3;

then ( ( z in G . A & not z in G . B ) or ( z in G . B & not z in G . A ) ) by A26, A22, A31, XBOOLE_0:def 4;

hence contradiction by A18; :: thesis: verum

rng G c= bool C

proof

then
card (rng G) c= card (bool C)
by CARD_1:11;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng G or a in bool C )

reconsider aa = a as set by TARSKI:1;

assume a in rng G ; :: thesis: a in bool C

then consider b being object such that

A34: b in dom G and

A35: a = G . b by FUNCT_1:def 3;

S_{1}[b,a]
by A14, A15, A34, A35;

then aa c= C by XBOOLE_1:17;

hence a in bool C ; :: thesis: verum

end;reconsider aa = a as set by TARSKI:1;

assume a in rng G ; :: thesis: a in bool C

then consider b being object such that

A34: b in dom G and

A35: a = G . b by FUNCT_1:def 3;

S

then aa c= C by XBOOLE_1:17;

hence a in bool C ; :: thesis: verum

then card (bool real-anti-diagonal) c= card (bool C) by A33, A14, XBOOLE_1:1;

then A36: exp (2,continuum) c= card (bool C) by CARD_2:31, Th3;

card (bool C) = exp (2,(card C)) by CARD_2:31;

then exp (2,continuum) c= exp (2,omega) by A36, A2, XBOOLE_1:1;

then exp (2,omega) in exp (2,omega) by A1, TOPGEN_3:29;

hence contradiction ; :: thesis: verum