set L = real-anti-diagonal ;
set S2 = Sorgenfrey-plane ;
reconsider C = as dense Subset of Sorgenfrey-plane by Th2;
defpred S1[ 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 ;
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 S1[a,b]
proof
let a be object ; :: thesis: ( a in bool real-anti-diagonal implies ex b being object st S1[a,b] )
assume a in bool real-anti-diagonal ; :: thesis: ex b being object st S1[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;
per cases ( a = {} or a = real-anti-diagonal or ( a <> {} & a <> real-anti-diagonal ) ) ;
end;
end;
consider G being Function such that
A14: dom G = bool real-anti-diagonal and
A15: for a being object st a in bool real-anti-diagonal holds
S1[a,G . a] from G is one-to-one
proof
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 ;
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 ;
A21: ( z in A \ B or z in B \ A ) by ;
S1[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 ;
S1[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 ;
A \ B = A /\ (B `) by SUBSET_1:13;
then A \ B c= UA /\ VB by ;
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 ;
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 ;
then ( ( z in UA & not z in UB ) or ( z in UB & not z in UA ) ) by ;
then ( ( z in G . A & not z in G . B ) or ( z in G . B & not z in G . A ) ) by ;
hence contradiction by A18; :: thesis: verum
end;
then A33: 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
A34: b in dom G and
A35: a = G . b by FUNCT_1:def 3;
S1[b,a] by A14, A15, A34, A35;
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 c= card (bool C) by ;
then A36: exp (2,continuum) c= card (bool C) by ;
card (bool C) = exp (2,(card C)) by CARD_2:31;
then exp (2,continuum) c= exp (2,omega) by ;
then exp (2,omega) in exp (2,omega) by ;
hence contradiction ; :: thesis: verum