let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) = {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
let n be Element of NAT ; :: thesis: (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) = {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
set US = (Cage C,n) -: (W-min (L~ (Cage C,n)));
set LS = (Cage C,n) :- (W-min (L~ (Cage C,n)));
set f = Cage C,n;
set pW = W-min (L~ (Cage C,n));
set pN = N-min (L~ (Cage C,n));
set pNa = N-max (L~ (Cage C,n));
set pSa = S-max (L~ (Cage C,n));
set pSi = S-min (L~ (Cage C,n));
set pEa = E-max (L~ (Cage C,n));
set pEi = E-min (L~ (Cage C,n));
A1: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
then A2: (Cage C,n) -: (W-min (L~ (Cage C,n))) <> {} by FINSEQ_5:50;
len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) = (W-min (L~ (Cage C,n))) .. (Cage C,n) by A1, FINSEQ_5:45;
then ((Cage C,n) -: (W-min (L~ (Cage C,n)))) /. (len ((Cage C,n) -: (W-min (L~ (Cage C,n))))) = W-min (L~ (Cage C,n)) by A1, FINSEQ_5:48;
then A3: W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A2, REVROT_1:3;
A4: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (E-min (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:75;
then (N-max (L~ (Cage C,n))) .. (Cage C,n) < (E-min (L~ (Cage C,n))) .. (Cage C,n) by A4, SPRECT_2:74, XXREAL_0:2;
then (N-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A4, SPRECT_2:76, XXREAL_0:2;
then A5: (N-max (L~ (Cage C,n))) .. (Cage C,n) < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A4, SPRECT_2:77, XXREAL_0:2;
((Cage C,n) -: (W-min (L~ (Cage C,n)))) /. 1 = (Cage C,n) /. 1 by A1, FINSEQ_5:47
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A6: N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A2, FINSEQ_6:46;
( N-max (L~ (Cage C,n)) in rng (Cage C,n) & (S-min (L~ (Cage C,n))) .. (Cage C,n) <= (W-min (L~ (Cage C,n))) .. (Cage C,n) ) by A4, SPRECT_2:44, SPRECT_2:78;
then A7: N-max (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A1, A5, FINSEQ_5:49, XXREAL_0:2;
{(N-min (L~ (Cage C,n))),(N-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(N-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} or x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(N-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))
hence x in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A6, A7, A3, ENUMSET1:def 1; :: thesis: verum

end;

then A8: card {(N-min (L~ (Cage C,n))),(N-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= card (rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))) by CARD_1:27;
((Cage C,n) :- (W-min (L~ (Cage C,n)))) /. 1 = W-min (L~ (Cage C,n)) by FINSEQ_5:56;
then A9: W-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by FINSEQ_6:46;
((Cage C,n) :- (W-min (L~ (Cage C,n)))) /. (len ((Cage C,n) :- (W-min (L~ (Cage C,n))))) = (Cage C,n) /. (len (Cage C,n)) by A1, FINSEQ_5:57
.= (Cage C,n) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A10: N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by REVROT_1:3;
{(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))
hence x in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by A10, A9, TARSKI:def 2; :: thesis: verum

end;

then A11: card {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= card (rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))) by CARD_1:27;
card (rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))) c= card (dom ((Cage C,n) :- (W-min (L~ (Cage C,n))))) by CARD_2:80;
then A12: card (rng ((Cage C,n) :- (W-min (L~ (Cage C,n))))) c= len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by CARD_1:104;
( W-max (L~ (Cage C,n)) in L~ (Cage C,n) & (N-min (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) ) by EUCLID:56, SPRECT_1:15;
then (W-max (L~ (Cage C,n))) `2 <= (N-min (L~ (Cage C,n))) `2 by PSCOMP_1:71;
then A13: N-min (L~ (Cage C,n)) <> W-min (L~ (Cage C,n)) by SPRECT_2:61;
then card {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} = 2 by CARD_2:76;
then 2 c= len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by A11, A12, XBOOLE_1:1;
then len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) >= 2 by NAT_1:40;
then A14: rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) c= L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by SPPOL_2:18;
((Cage C,n) :- (W-min (L~ (Cage C,n)))) /. (len ((Cage C,n) :- (W-min (L~ (Cage C,n))))) = (Cage C,n) /. (len (Cage C,n)) by A1, FINSEQ_5:57
.= (Cage C,n) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A15: N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by REVROT_1:3;
(W-min (L~ (Cage C,n))) .. (Cage C,n) <= (W-min (L~ (Cage C,n))) .. (Cage C,n) ;
then A16: ( W-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (W-min (L~ (Cage C,n)))) & W-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) ) by A1, FINSEQ_5:49, FINSEQ_6:66;
( W-max (L~ (Cage C,n)) in L~ (Cage C,n) & (N-max (L~ (Cage C,n))) `2 = N-bound (L~ (Cage C,n)) ) by EUCLID:56, SPRECT_1:15;
then (W-max (L~ (Cage C,n))) `2 <= (N-max (L~ (Cage C,n))) `2 by PSCOMP_1:71;
then ( N-min (L~ (Cage C,n)) <> N-max (L~ (Cage C,n)) & N-max (L~ (Cage C,n)) <> W-min (L~ (Cage C,n)) ) by SPRECT_2:56, SPRECT_2:61;
then A17: card {(N-min (L~ (Cage C,n))),(N-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} = 3 by A13, CARD_2:77;
card (rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))) c= card (dom ((Cage C,n) -: (W-min (L~ (Cage C,n))))) by CARD_2:80;
then card (rng ((Cage C,n) -: (W-min (L~ (Cage C,n))))) c= len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by CARD_1:104;
then 3 c= len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A17, A8, XBOOLE_1:1;
then A18: len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) >= 3 by NAT_1:40;
then A19: rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) c= L~ ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by SPPOL_2:18, XXREAL_0:2;
thus (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) c= {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} :: according to XBOOLE_0:def 10 :: thesis: {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) or x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} )
assume A20: x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) ; :: thesis: x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
then reconsider x1 = x as Point of (TOP-REAL 2) ;
assume A21: not x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: contradiction
x in L~ ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A20, XBOOLE_0:def 4;
then consider i1 being Element of NAT such that
A22: 1 <= i1 and
A23: i1 + 1 <= len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) and
A24: x1 in LSeg ((Cage C,n) -: (W-min (L~ (Cage C,n)))),i1 by SPPOL_2:13;
A25: LSeg ((Cage C,n) -: (W-min (L~ (Cage C,n)))),i1 = LSeg (Cage C,n),i1 by A23, SPPOL_2:9;
x in L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))) by A20, XBOOLE_0:def 4;
then consider i2 being Element of NAT such that
A26: 1 <= i2 and
A27: i2 + 1 <= len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) and
A28: x1 in LSeg ((Cage C,n) :- (W-min (L~ (Cage C,n)))),i2 by SPPOL_2:13;
set i3 = i2 -' 1;
A29: (i2 -' 1) + 1 = i2 by A26, XREAL_1:237;
then A30: 1 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) <= ((i2 -' 1) + 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A26, XREAL_1:9;
A31: len ((Cage C,n) :- (W-min (L~ (Cage C,n)))) = ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 by A1, FINSEQ_5:53;
then i2 < ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 by A27, NAT_1:13;
then i2 - 1 < (len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1:21;
then A32: (i2 - 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) < len (Cage C,n) by XREAL_1:22;
i2 - 1 >= 1 - 1 by A26, XREAL_1:11;
then A33: (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) < len (Cage C,n) by A32, XREAL_0:def 2;
A34: LSeg ((Cage C,n) :- (W-min (L~ (Cage C,n)))),i2 = LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) by A1, A29, SPPOL_2:10;
A35: len ((Cage C,n) -: (W-min (L~ (Cage C,n)))) = (W-min (L~ (Cage C,n))) .. (Cage C,n) by A1, FINSEQ_5:45;
then i1 + 1 < ((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1 by A23, NAT_1:13;
then i1 + 1 < ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 by A30, XXREAL_0:2;
then A36: i1 + 1 <= (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by NAT_1:13;
A37: (((W-min (L~ (Cage C,n))) .. (Cage C,n)) -' 1) + 1 = (W-min (L~ (Cage C,n))) .. (Cage C,n) by A1, FINSEQ_4:31, XREAL_1:237;
(i2 -' 1) + 1 < ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 by A27, A29, A31, NAT_1:13;
then i2 -' 1 < (len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1:9;
then A38: (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) < len (Cage C,n) by XREAL_1:22;
then A39: ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 <= len (Cage C,n) by NAT_1:13;

now

per cases ( ( i1 + 1 < (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) & i1 > 1 ) or i1 = 1 or i1 + 1 = (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) ) by A22, A36, XXREAL_0:1;

suppose ( i1 + 1 < (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) & i1 > 1 ) ; :: thesis: contradiction

then LSeg (Cage C,n),i1 misses LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) by A38, GOBOARD5:def 4;
then (LSeg (Cage C,n),i1) /\ (LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) = {} by XBOOLE_0:def 7;
hence contradiction by A24, A28, A25, A34, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A40: i1 = 1 ; :: thesis: contradiction

(i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) >= 0 + 3 by A18, A35, XREAL_1:9;
then A41: i1 + 1 < (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by A40, XXREAL_0:2;

now

per cases ( ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 < len (Cage C,n) or ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 = len (Cage C,n) ) by A39, XXREAL_0:1;

suppose ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 < len (Cage C,n) ; :: thesis: contradiction

then LSeg (Cage C,n),i1 misses LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) by A41, GOBOARD5:def 4;
then (LSeg (Cage C,n),i1) /\ (LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) = {} by XBOOLE_0:def 7;
hence contradiction by A24, A28, A25, A34, XBOOLE_0:def 4; :: thesis: verum

end;

suppose ((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1 = len (Cage C,n) ; :: thesis: contradiction

then (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = (len (Cage C,n)) - 1 ;
then (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) = (len (Cage C,n)) -' 1 by XREAL_0:def 2;
then (LSeg (Cage C,n),i1) /\ (LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) = {((Cage C,n) /. 1)} by A40, GOBOARD7:36, REVROT_1:30;
then x1 in {((Cage C,n) /. 1)} by A24, A28, A25, A34, XBOOLE_0:def 4;
then x1 = (Cage C,n) /. 1 by TARSKI:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
hence contradiction by A21, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A42: i1 + 1 = (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) ; :: thesis: contradiction

(i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) >= (W-min (L~ (Cage C,n))) .. (Cage C,n) by NAT_1:11;
then (W-min (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A33, XXREAL_0:2;
then ((W-min (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) by NAT_1:13;
then A43: (((W-min (L~ (Cage C,n))) .. (Cage C,n)) -' 1) + (1 + 1) <= len (Cage C,n) by A37;
0 + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) <= (i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by XREAL_1:9;
then (W-min (L~ (Cage C,n))) .. (Cage C,n) = i1 + 1 by A23, A35, A42, XXREAL_0:1;
then (LSeg (Cage C,n),i1) /\ (LSeg (Cage C,n),((i2 -' 1) + ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) = {((Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)))} by A22, A37, A42, A43, TOPREAL1:def 8;
then x1 in {((Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)))} by A24, A28, A25, A34, XBOOLE_0:def 4;
then x1 = (Cage C,n) /. ((W-min (L~ (Cage C,n))) .. (Cage C,n)) by TARSKI:def 1
.= W-min (L~ (Cage C,n)) by A1, FINSEQ_5:41 ;
hence contradiction by A21, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A44: ((Cage C,n) -: (W-min (L~ (Cage C,n)))) /. 1 = (Cage C,n) /. 1 by A1, FINSEQ_5:47
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
not (Cage C,n) -: (W-min (L~ (Cage C,n))) is empty by A17, A8, NAT_1:40;
then A45: N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (W-min (L~ (Cage C,n)))) by A44, FINSEQ_6:46;
thus {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} c= (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} or x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) )
assume A46: x in {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))} ; :: thesis: x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))))

per cases ( x = N-min (L~ (Cage C,n)) or x = W-min (L~ (Cage C,n)) ) by A46, TARSKI:def 2;

suppose x = N-min (L~ (Cage C,n)) ; :: thesis: x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))))

hence x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) by A14, A19, A45, A15, XBOOLE_0:def 4; :: thesis: verum

end;

suppose x = W-min (L~ (Cage C,n)) ; :: thesis: x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n)))))

hence x in (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) by A14, A19, A16, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;