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:65;
A2: Cl (RightComp (SpStSeq C)) = (RightComp (SpStSeq C)) \/ (L~ (SpStSeq C)) by Th31;

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 set ; :: 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 set 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 set ; :: 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

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

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:66;

now

per cases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def 3;

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 Th33, Th34;
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;

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:71;
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;

end;

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

end;

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:66;

now

per cases ( a in RightComp (SpStSeq C) or a in L~ (SpStSeq C) ) by A2, A3, XBOOLE_0:def 3;

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 Th35, Th36;
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;

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:71;
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;

end;

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

end;

end;

end;

a is Tuple of 2, REAL by A3, Lm1, FINSEQ_2:151;
then ex r, s being Real st a = <*r,s*> by FINSEQ_2:120;
then dom h = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
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:18; :: thesis: verum

end;

let a be set ; :: 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)) )
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 set 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:66;
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:66;
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:54;
A20: for k being set st k in dom h holds
h . k = <*r,s*> . k

proof

let k be set ; :: 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:61; :: thesis: verum

end;

dom <*r,s*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
then A21: a = |[r,s]| by A10, A11, A20, FUNCT_1:9, FUNCT_4:65;
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, Th26;
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:56; :: thesis: verum