reconsider C = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) as dense Subset of Niemytzki-plane by Th36;
set T = Niemytzki-plane ;
defpred S₁[ object , object ] means ex D1 being set ex U, V being open Subset of Niemytzki-plane st
( D1 = $1 & $2 = U /\ C & D1 c= U & y=0-line \ D1 c= V & U misses V );
A1: exp (2,omega) in exp (2,(exp (2,omega))) by CARD_5:14;
card C c= card (product <*RAT,RAT*>) by CARD_1:11, XBOOLE_1:17;
then card C c= omega by Th8, CARD_4:6, TOPGEN_3:17;
then A2: exp (2,(card C)) c= exp (2,omega) by CARD_2:93;
assume A3: for W, V being Subset of Niemytzki-plane st W <> {} & V <> {} & W is closed & V is closed & W misses V holds
ex P, Q being Subset of Niemytzki-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 y=0-line holds
ex b being object st S₁[a,b]

proof

let a be object ; :: thesis: ( a in bool y=0-line implies ex b being object st S₁[a,b] )
assume a in bool y=0-line ; :: thesis: ex b being object st S₁[a,b]
then reconsider aa = a as Subset of y=0-line ;
reconsider a9 = y=0-line \ aa as Subset of y=0-line by XBOOLE_1:36;
reconsider A = aa, B = a9 as closed Subset of Niemytzki-plane by Th42;

per cases ( a = {} or a = y=0-line or ( a <> {} & a <> y=0-line ) ) ;

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

take {} ; :: thesis: S₁[a, {} ]
take {} ; :: thesis: ex U, V being open Subset of Niemytzki-plane st
( {} = a & {} = U /\ C & {} c= U & y=0-line \ {} c= V & U misses V )
take {} Niemytzki-plane ; :: thesis: ex V being open Subset of Niemytzki-plane st
( {} = a & {} = ({} Niemytzki-plane) /\ C & {} c= {} Niemytzki-plane & y=0-line \ {} c= V & {} Niemytzki-plane misses V )
take [#] Niemytzki-plane ; :: thesis: ( {} = a & {} = ({} Niemytzki-plane) /\ C & {} c= {} Niemytzki-plane & y=0-line \ {} c= [#] Niemytzki-plane & {} Niemytzki-plane misses [#] Niemytzki-plane )
thus ( {} = a & {} = ({} Niemytzki-plane) /\ C & {} c= {} Niemytzki-plane & y=0-line \ {} c= [#] Niemytzki-plane & {} Niemytzki-plane misses [#] Niemytzki-plane ) by A5, Def3, Th19; :: thesis: verum

end;

suppose A6: a = y=0-line ; :: thesis: ex b being object st S₁[a,b]

take ([#] Niemytzki-plane) /\ C ; :: thesis: S₁[a,([#] Niemytzki-plane) /\ C]
take aa ; :: thesis: ex U, V being open Subset of Niemytzki-plane st
( aa = a & ([#] Niemytzki-plane) /\ C = U /\ C & aa c= U & y=0-line \ aa c= V & U misses V )
take [#] Niemytzki-plane ; :: thesis: ex V being open Subset of Niemytzki-plane st
( aa = a & ([#] Niemytzki-plane) /\ C = ([#] Niemytzki-plane) /\ C & aa c= [#] Niemytzki-plane & y=0-line \ aa c= V & [#] Niemytzki-plane misses V )
take {} Niemytzki-plane ; :: thesis: ( aa = a & ([#] Niemytzki-plane) /\ C = ([#] Niemytzki-plane) /\ C & aa c= [#] Niemytzki-plane & y=0-line \ aa c= {} Niemytzki-plane & [#] Niemytzki-plane misses {} Niemytzki-plane )
thus aa = a ; :: thesis: ( ([#] Niemytzki-plane) /\ C = ([#] Niemytzki-plane) /\ C & aa c= [#] Niemytzki-plane & y=0-line \ aa c= {} Niemytzki-plane & [#] Niemytzki-plane misses {} Niemytzki-plane )
thus ( ([#] Niemytzki-plane) /\ C = ([#] Niemytzki-plane) /\ C & aa c= [#] Niemytzki-plane & y=0-line \ aa c= {} Niemytzki-plane & [#] Niemytzki-plane misses {} Niemytzki-plane ) by A6, Def3, Th19, XBOOLE_1:37; :: thesis: verum

end;

suppose A7: ( a <> {} & a <> y=0-line ) ; :: thesis: ex b being object st S₁[a,b]

(aa `) ` = a9 ` ;
then A8: B <> {} y=0-line by A7;
A misses B by XBOOLE_1:79;
then consider P, Q being Subset of Niemytzki-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₁[a,P /\ C]
thus S₁[a,P /\ C] by A9, A10, A11, A12, A13; :: thesis: verum

end;

end;

end;

consider G being Function such that
A14: dom G = bool y=0-line and
A15: for a being object st a in bool y=0-line holds
S₁[a,G . a] from CLASSES1:sch 1(A4);
G is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 G or not y in proj1 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 y=0-line 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;
consider D1 being set , UB, VB being open Subset of Niemytzki-plane such that
A22: D1 = B and
A23: G . B = UB /\ C and
A24: D1 c= UB and
A25: y=0-line \ D1 c= VB and
A26: UB misses VB by A15;
consider D1 being set , UA, VA being open Subset of Niemytzki-plane such that
A27: D1 = A and
A28: G . A = UA /\ C and
A29: D1 c= UA and
A30: y=0-line \ D1 c= VA and
A31: UA misses VA by A15;
B \ A = B /\ (A `) by SUBSET_1:13;
then A32: B \ A c= UB /\ VA by A30, A24, XBOOLE_1:27, A22, A27;
A \ B = A /\ (B `) by SUBSET_1:13;
then A \ B c= UA /\ VB by A29, A25, XBOOLE_1:27, A22, A27;
then ( C meets UA /\ VB or C meets UB /\ VA ) by A32, A21, TOPS_1:45;
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;
then consider z being set such that
A33: z in C and
A34: ( z in UA /\ VB or z in UB /\ VA ) ;
( ( z in UA & z in VB ) or ( z in UB & z in VA ) ) by A34, XBOOLE_0:def 4;
then ( ( z in UA & not z in UB ) or ( z in UB & not z in UA ) ) by A31, A26, XBOOLE_0:3;
then ( ( z in G . A & not z in G . B ) or ( z in G . B & not z in G . A ) ) by A28, A23, A33, XBOOLE_0:def 4;
hence contradiction by A18; :: thesis: verum

end;

then A35: card (dom G) c= card (rng G) by CARD_1:10;
rng G c= bool C

proof

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
A36: b in dom G and
A37: a = G . b by FUNCT_1:def 3;
S₁[b,aa] by A14, A15, A36, A37;
then aa c= C by XBOOLE_1:17;
hence a in bool C ; :: thesis: verum

end;

then card (rng G) c= card (bool C) by CARD_1:11;
then card (bool y=0-line) c= card (bool C) by A35, A14;
then A38: exp (2,continuum) c= card (bool C) by Th16, CARD_2:31;
card (bool C) = exp (2,(card C)) by CARD_2:31;
then exp (2,continuum) c= exp (2,omega) by A38, A2;
then exp (2,omega) in exp (2,omega) by A1, TOPGEN_3:29;
hence contradiction ; :: thesis: verum