set T = Niemytzki-plane ;
assume A1: 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 6 :: thesis: contradiction
reconsider C = (y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) as dense Subset of Niemytzki-plane by Th40;
defpred S₁[ set , set ] means ex U, V being open Subset of Niemytzki-plane st
( $2 = U /\ C & $1 c= U & y=0-line \ $1 c= V & U misses V );
A2: for a being set st a in bool y=0-line holds
ex b being set st S₁[a,b]

proof

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

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

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

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

end;

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

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

end;

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

( (aa ` ) ` = a' ` & (aa ` ) ` = a & ({} y=0-line ) ` = [#] y=0-line ) ;
then ( B <> {} y=0-line & A misses B ) by A5, XBOOLE_1:79;
then consider P, Q being Subset of Niemytzki-plane such that
A6: ( P is open & Q is open & A c= P & B c= Q & P misses Q ) by A1, A5;
take b = P /\ C; :: thesis: S₁[a,b]
thus S₁[a,b] by A6; :: thesis: verum

end;

end;

end;

consider G being Function such that
A7: dom G = bool y=0-line and
A8: for a being set st a in bool y=0-line holds
S₁[a,G . a] from CLASSES1:sch 1(A2);
rng G c= bool C

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng G or a in bool C )
assume a in rng G ; :: thesis: a in bool C
then consider b being set such that
A9: ( b in dom G & a = G . b ) by FUNCT_1:def 5;
S₁[b,a] by A7, A8, A9;
then a c= C by XBOOLE_1:17;
hence a in bool C ; :: thesis: verum

end;

then A10: card (rng G) c= card (bool C) by CARD_1:27;
card C c= card (product <*RAT ,RAT *>) by CARD_1:27, XBOOLE_1:17;
then card C c= omega by Th12, CARD_4:54, TOPGEN_3:17;
then A11: ( card (bool C) = exp 2,(card C) & exp 2,(card C) c= exp 2,omega ) by CARD_2:44, CARD_3:139;
G is one-to-one

proof

let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 G or not y in proj1 G or not G . x = G . y or x = y )
assume ( x in dom G & y in dom G ) ; :: thesis: ( not G . x = G . y or x = y )
then reconsider A = x, B = y as Subset of y=0-line by A7;
consider UA, VA being open Subset of Niemytzki-plane such that
A12: ( G . A = UA /\ C & A c= UA & y=0-line \ A c= VA & UA misses VA ) by A8;
consider UB, VB being open Subset of Niemytzki-plane such that
A13: ( G . B = UB /\ C & B c= UB & y=0-line \ B c= VB & UB misses VB ) by A8;
assume A14: ( G . x = G . y & x <> y ) ; :: thesis: contradiction
then consider z being set such that
A15: ( ( z in A & not z in B ) or ( z in B & not z in A ) ) by TARSKI:2;
A16: ( z in A \ B or z in B \ A ) by A15, XBOOLE_0:def 5;
( A ` = y=0-line \ A & B ` = y=0-line \ B & A \ B = A /\ (B ` ) & B \ A = B /\ (A ` ) ) by SUBSET_1:32;
then ( A \ B c= UA /\ VB & B \ A c= UB /\ VA ) by A12, A13, XBOOLE_1:27;
then ( ( z in UA /\ VB & UA /\ VB is open ) or ( z in UB /\ VA & UB /\ VA is open ) ) by A16, TOPS_1:38;
then ( C meets UA /\ VB or C meets UB /\ VA ) by TOPS_1:80;
then ( ex z being set st
( z in C & z in UA /\ VB ) or ex z being set st
( z in C & z in UB /\ VA ) ) by XBOOLE_0:3;
then consider z being set such that
A17: ( z in C & ( z in UA /\ VB or z in UB /\ VA ) ) ;
( ( z in UA & z in VB ) or ( z in UB & z in VA ) ) by A17, XBOOLE_0:def 4;
then ( ( z in UA & not z in UB ) or ( z in UB & not z in UA ) ) by A12, A13, XBOOLE_0:3;
then ( ( z in G . A & not z in G . B ) or ( z in G . B & not z in G . A ) ) by A12, A13, A17, XBOOLE_0:def 4;
hence contradiction by A14; :: thesis: verum

end;

then card (dom G) c= card (rng G) by CARD_1:26;
then card (bool y=0-line ) c= card (bool C) by A7, A10, XBOOLE_1:1;
then exp 2,continuum c= card (bool C) by Th20, CARD_2:44;
then ( exp 2,continuum c= exp 2,omega & exp 2,omega in exp 2,(exp 2,omega ) ) by A11, CARD_5:23, XBOOLE_1:1;
then exp 2,omega in exp 2,omega by TOPGEN_3:29;
hence contradiction ; :: thesis: verum