let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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;

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))).])) ; :: thesis: 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

then A21: a = |[r,s]| by A10, A11, A20, FUNCT_1:2, FUNCT_4:62;

assume not a in Cl (RightComp (SpStSeq C)) ; :: thesis: 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; :: thesis: verum

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 :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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)) )let a be object ; :: thesis: ( 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)) ; :: thesis: 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

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; :: thesis: verum

end;assume A3: a in Cl (RightComp (SpStSeq C)) ; :: thesis: 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

a is Tuple of 2, REAL
by A3, Lm1, FINSEQ_2:131;
let x be object ; :: thesis: ( 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} ; :: thesis: 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;assume A5: x in {1,2} ; :: thesis: 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

per cases
( x = 1 or x = 2 )
by A5, TARSKI:def 2;

end;

suppose A6:
x = 1
; :: thesis: 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

then A7:
((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).]
by FUNCT_4:63;

end;now :: thesis: ( ( a in RightComp (SpStSeq C) & 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 ) or ( a in L~ (SpStSeq C) & 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;

hence
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
; :: thesis: verumper cases
( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) )
by A2, A3, XBOOLE_0:def 3;

end;

case
a in RightComp (SpStSeq C)
; :: thesis: 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

then
( W-bound (L~ (SpStSeq C)) < b `1 & E-bound (L~ (SpStSeq C)) > b `1 )
by Th23, Th24;

hence 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 A6, A7, XXREAL_1:1; :: thesis: verum

end;hence 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 A6, A7, XXREAL_1:1; :: thesis: verum

case
a in L~ (SpStSeq C)
; :: thesis: 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

then
( W-bound (L~ (SpStSeq C)) <= b `1 & b `1 <= E-bound (L~ (SpStSeq C)) )
by PSCOMP_1:24;

hence 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 A6, A7, XXREAL_1:1; :: thesis: verum

end;hence 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 A6, A7, XXREAL_1:1; :: thesis: verum

suppose A8:
x = 2
; :: thesis: 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

then A9:
((1,2) --> ([.(W-bound (L~ (SpStSeq C))),(E-bound (L~ (SpStSeq C))).],[.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).])) . x = [.(S-bound (L~ (SpStSeq C))),(N-bound (L~ (SpStSeq C))).]
by FUNCT_4:63;

end;now :: thesis: ( ( a in RightComp (SpStSeq C) & 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 ) or ( a in L~ (SpStSeq C) & 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;

hence
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
; :: thesis: verumper cases
( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) )
by A2, A3, XBOOLE_0:def 3;

end;

case
a in RightComp (SpStSeq C)
; :: thesis: 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

then
( S-bound (L~ (SpStSeq C)) < b `2 & N-bound (L~ (SpStSeq C)) > b `2 )
by Th25, Th26;

hence 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 A8, A9, XXREAL_1:1; :: thesis: verum

end;hence 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 A8, A9, XXREAL_1:1; :: thesis: verum

case
a in L~ (SpStSeq C)
; :: thesis: 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

then
( S-bound (L~ (SpStSeq C)) <= b `2 & b `2 <= N-bound (L~ (SpStSeq C)) )
by PSCOMP_1:24;

hence 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 A8, A9, XXREAL_1:1; :: thesis: verum

end;hence 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 A8, A9, XXREAL_1:1; :: thesis: verum

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; :: thesis: verum

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))).])) ; :: thesis: 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

proof

dom <*r,s*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
let k be object ; :: thesis: ( k in dom h implies h . k = <*r,s*> . k )

assume k in dom h ; :: thesis: h . k = <*r,s*> . k

then ( k = 1 or k = 2 ) by A11, TARSKI:def 2;

hence h . k = <*r,s*> . k by A17, A14, FINSEQ_1:44; :: thesis: verum

end;assume k in dom h ; :: thesis: h . k = <*r,s*> . k

then ( k = 1 or k = 2 ) by A11, TARSKI:def 2;

hence h . k = <*r,s*> . k by A17, A14, FINSEQ_1:44; :: thesis: verum

then A21: a = |[r,s]| by A10, A11, A20, FUNCT_1:2, FUNCT_4:62;

assume not a in Cl (RightComp (SpStSeq C)) ; :: thesis: 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; :: thesis: verum