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;
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 ; :: 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
proof
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
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:63;
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 ) )
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 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;
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;
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:63;
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 ) )
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 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;
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;
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: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; :: thesis: verum
end;
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)) )
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
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;
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)) ; :: 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