set L = real-anti-diagonal ;
set S2 = Sorgenfrey-plane ;
reconsider C = [:RAT,RAT:] 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 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 )
; COMPTS_1:def 3 contradiction
A4:
for a being object st a in bool real-anti-diagonal holds
ex b being object st S1[a,b]
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 CLASSES1:sch 1(A4);
G is one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( 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
;
( 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
;
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;
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 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;
verum
end;
then A33:
card (dom G) c= card (rng G)
by CARD_1:10;
rng G c= bool C
then
card (rng G) c= card (bool C)
by CARD_1:11;
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
; verum