let C be compact non horizontal non vertical Subset of (TOP-REAL 2); Cl (RightComp (SpStSeq C)) = product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
set g = (1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]);
A1:
dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) = {1,2}
by FUNCT_4:62;
A2:
Cl (RightComp (SpStSeq C)) = (RightComp (SpStSeq C)) \/ (L~ (SpStSeq C))
by Th21;
hereby TARSKI:def 3,
XBOOLE_0:def 10 product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) c= Cl (RightComp (SpStSeq C))
let a be
object ;
( a in Cl (RightComp (SpStSeq C)) implies a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) )assume A3:
a in Cl (RightComp (SpStSeq C))
;
a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))then reconsider b =
a as
Point of
(TOP-REAL 2) ;
reconsider h =
a as
FinSequence by A3;
A4:
for
x being
object st
x in {1,2} holds
h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
proof
let x be
object ;
( x in {1,2} implies h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x )
assume A5:
x in {1,2}
;
h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
end;
a is
Tuple of 2,
REAL
by A3, Lm1, FINSEQ_2:131;
then
ex
r,
s being
Element of
REAL st
a = <*r,s*>
by FINSEQ_2:100;
then
dom h = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
hence
a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
by A1, A4, CARD_3:9;
verum
end;
let a be object ; TARSKI:def 3 ( not a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) or a in Cl (RightComp (SpStSeq C)) )
assume
a in product ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
; a in Cl (RightComp (SpStSeq C))
then consider h being Function such that
A10:
a = h
and
A11:
dom h = dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
and
A12:
for x being object st x in dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) holds
h . x in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x
by CARD_3:def 5;
A13:
[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).] = { s where s is Real : ( S-bound (L~ (SpStSeq C)) <= s & s <= N-bound (L~ (SpStSeq C)) ) }
by RCOMP_1:def 1;
2 in dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
by A1, TARSKI:def 2;
then
h . 2 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 2
by A12;
then
h . 2 in [.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]
by FUNCT_4:63;
then consider s being Real such that
A14:
h . 2 = s
and
A15:
( S-bound (L~ (SpStSeq C)) <= s & s <= N-bound (L~ (SpStSeq C)) )
by A13;
A16:
[.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).] = { r where r is Real : ( W-bound (L~ (SpStSeq C)) <= r & r <= E-bound (L~ (SpStSeq C)) ) }
by RCOMP_1:def 1;
1 in dom ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]))
by A1, TARSKI:def 2;
then
h . 1 in ((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . 1
by A12;
then
h . 1 in [.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).]
by FUNCT_4:63;
then consider r being Real such that
A17:
h . 1 = r
and
A18:
( W-bound (L~ (SpStSeq C)) <= r & r <= E-bound (L~ (SpStSeq C)) )
by A16;
A19:
LeftComp (SpStSeq C) = { q where q is Point of (TOP-REAL 2) : ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) }
by SPRECT_3:37;
A20:
for k being object st k in dom h holds
h . k = <*r,s*> . k
dom <*r,s*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then A21:
a = |[r,s]|
by A10, A11, A20, FUNCT_1:2, FUNCT_4:62;
assume
not a in Cl (RightComp (SpStSeq C))
; contradiction
then
( not a in RightComp (SpStSeq C) & not a in L~ (SpStSeq C) )
by A2, XBOOLE_0:def 3;
then
a in LeftComp (SpStSeq C)
by A21, Th16;
then
ex q being Point of (TOP-REAL 2) st
( q = a & ( not W-bound (L~ (SpStSeq C)) <= q `1 or not q `1 <= E-bound (L~ (SpStSeq C)) or not S-bound (L~ (SpStSeq C)) <= q `2 or not q `2 <= N-bound (L~ (SpStSeq C)) ) )
by A19;
hence
contradiction
by A18, A15, A21, EUCLID:52; verum