let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
let n be Nat; :: thesis: (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
set US = (Cage (C,n)) -: (E-max (L~ (Cage (C,n))));
set LS = (Cage (C,n)) :- (E-max (L~ (Cage (C,n))));
set f = Cage (C,n);
set pW = E-max (L~ (Cage (C,n)));
set pN = N-min (L~ (Cage (C,n)));
A1: (E-max (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) by EUCLID:52;
A2: E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A3: (Cage (C,n)) -: (E-max (L~ (Cage (C,n)))) <> {} by FINSEQ_5:47;
((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. 1 = E-max (L~ (Cage (C,n))) by FINSEQ_5:53;
then A4: E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_6:42;
((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = (Cage (C,n)) /. (len (Cage (C,n))) by A2, FINSEQ_5:54
.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
then A5: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_6:168;
{(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by A5, A4, TARSKI:def 2;
then A6: card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) by CARD_1:11;
card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) by CARD_2:61;
then A7: card (rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by CARD_1:62;
N-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) by SPRECT_1:11;
then (N-max (L~ (Cage (C,n)))) `1 <= (E-max (L~ (Cage (C,n)))) `1 by A1, PSCOMP_1:24;
then A8: N-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) by SPRECT_2:51;
then card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} = 2 by CARD_2:57;
then Segm 2 c= Segm (len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) by A6, A7;
then len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) >= 2 by NAT_1:39;
then A9: rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by SPPOL_2:18;
len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, FINSEQ_5:42;
then ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) = E-max (L~ (Cage (C,n))) by A2, FINSEQ_5:45;
then A10: E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A3, FINSEQ_6:168;
((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. 1 = (Cage (C,n)) /. 1 by A2, FINSEQ_5:44
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
then A11: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A3, FINSEQ_6:42;
{(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A11, A10, TARSKI:def 2;
then A12: card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) by CARD_1:11;
card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) by CARD_2:61;
then A13: card (rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by CARD_1:62;
((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) = (Cage (C,n)) /. (len (Cage (C,n))) by A2, FINSEQ_5:54
.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
then A14: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_6:168;
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) ;
then A15: E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A2, FINSEQ_5:46;
card {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} = 2 by A8, CARD_2:57;
then A16: Segm 2 c= Segm (len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) by A12, A13;
then A17: len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) >= 2 by NAT_1:39;
then A18: rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) c= L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by SPPOL_2:18;
thus (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) c= {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} :: according to XBOOLE_0:def 10 :: thesis: {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) or x in {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} )
assume A19: x in (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) ; :: thesis: x in {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
then reconsider x1 = x as Point of (TOP-REAL 2) ;
assume A20: not x in {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; :: thesis: contradiction
x in L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A19, XBOOLE_0:def 4;
then consider i1 being Nat such that
A21: 1 <= i1 and
A22: i1 + 1 <= len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) and
A23: x1 in LSeg (((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))),i1) by SPPOL_2:13;
A24: LSeg (((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))),i1) = LSeg ((Cage (C,n)),i1) by A22, SPPOL_2:9;
x in L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by A19, XBOOLE_0:def 4;
then consider i2 being Nat such that
A25: 1 <= i2 and
A26: i2 + 1 <= len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) and
A27: x1 in LSeg (((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))),i2) by SPPOL_2:13;
set i3 = i2 -' 1;
A28: (i2 -' 1) + 1 = i2 by A25, XREAL_1:235;
then A29: 1 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= ((i2 -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by A25, XREAL_1:7;
A30: len ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) = ((len (Cage (C,n))) - ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A2, FINSEQ_5:50;
then i2 < ((len (Cage (C,n))) - ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A26, NAT_1:13;
then i2 - 1 < (len (Cage (C,n))) - ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:19;
then A31: (i2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;
i2 - 1 >= 1 - 1 by A25, XREAL_1:9;
then A32: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by A31, XREAL_0:def 2;
A33: LSeg (((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))),i2) = LSeg ((Cage (C,n)),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A2, A28, SPPOL_2:10;
A34: len ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, FINSEQ_5:42;
then i1 + 1 < ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by A22, NAT_1:13;
then i1 + 1 < ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A29, XXREAL_0:2;
then A35: i1 + 1 <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by NAT_1:13;
A36: (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + 1 = (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, FINSEQ_4:21, XREAL_1:235;
(i2 -' 1) + 1 < ((len (Cage (C,n))) - ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A26, A28, A30, NAT_1:13;
then i2 -' 1 < (len (Cage (C,n))) - ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;
then A37: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;
then A38: ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= len (Cage (C,n)) by NAT_1:13;

now :: thesis: contradiction

per cases ( ( i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) & i1 > 1 ) or i1 = 1 or i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) ) by A21, A35, XXREAL_0:1;

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

then LSeg ((Cage (C,n)),i1) misses LSeg ((Cage (C,n)),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A37, GOBOARD5:def 4;
then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;
hence contradiction by A23, A27, A24, A33, XBOOLE_0:def 4; :: thesis: verum

end;

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

A40: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) >= 0 + 2 by A17, A34, XREAL_1:7;

now :: thesis: contradiction

per cases ( (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) > 2 or (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = 2 ) by A40, XXREAL_0:1;

suppose (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) > 2 ; :: thesis: contradiction

then A41: i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by A39;

now :: thesis: contradiction

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

suppose ((i2 -' 1) + ((E-max (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) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))))) by A41, GOBOARD5:def 4;
then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;
hence contradiction by A23, A27, A24, A33, XBOOLE_0:def 4; :: thesis: verum

end;

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

then (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = (len (Cage (C,n))) - 1 ;
then (i2 -' 1) + ((E-max (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) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {((Cage (C,n)) /. 1)} by A39, GOBOARD7:34, REVROT_1:30;
then x1 in {((Cage (C,n)) /. 1)} by A23, A27, A24, A33, XBOOLE_0:def 4;
then x1 = (Cage (C,n)) /. 1 by TARSKI:def 1
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
hence contradiction by A20, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A42: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) = 2 ; :: thesis: contradiction

A43: 1 + 2 <= len (Cage (C,n)) by GOBOARD7:34, XXREAL_0:2;
x1 in (LSeg ((Cage (C,n)),1)) /\ (LSeg ((Cage (C,n)),(1 + 1))) by A23, A27, A24, A33, A39, A42, XBOOLE_0:def 4;
then x1 in {((Cage (C,n)) /. (1 + 1))} by A43, TOPREAL1:def 6;
then A44: x1 = (Cage (C,n)) /. (1 + 1) by TARSKI:def 1;
0 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) >= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by A16, A34, A42, NAT_1:39;
then A45: i2 -' 1 = 0 by XREAL_1:6;
0 + 1 in dom ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_5:6;
then ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) /. 1 = x1 by A2, A42, A44, A45, FINSEQ_5:52;
then x1 = E-max (L~ (Cage (C,n))) by FINSEQ_5:53;
hence contradiction by A20, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A46: i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) ; :: thesis: contradiction

(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) >= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by NAT_1:11;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A32, XXREAL_0:2;
then ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;
then A47: (((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + (1 + 1) <= len (Cage (C,n)) by A36;
0 + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;
then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) = i1 + 1 by A22, A34, A46, XXREAL_0:1;
then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {((Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))))} by A21, A36, A46, A47, TOPREAL1:def 6;
then x1 in {((Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))))} by A23, A27, A24, A33, XBOOLE_0:def 4;
then x1 = (Cage (C,n)) /. ((E-max (L~ (Cage (C,n)))) .. (Cage (C,n))) by TARSKI:def 1
.= E-max (L~ (Cage (C,n))) by A2, FINSEQ_5:38 ;
hence contradiction by A20, TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A48: ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) /. 1 = (Cage (C,n)) /. 1 by A2, FINSEQ_5:44
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
not (Cage (C,n)) -: (E-max (L~ (Cage (C,n)))) is empty by A16, NAT_1:39;
then A49: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (E-max (L~ (Cage (C,n))))) by A48, FINSEQ_6:42;
A50: E-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_6:61;
thus {(N-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) :: thesis: verum

proof

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

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

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

hence x in (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) by A9, A18, A49, A14, XBOOLE_0:def 4; :: thesis: verum

end;

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

hence x in (L~ ((Cage (C,n)) -: (E-max (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (E-max (L~ (Cage (C,n)))))) by A9, A50, A18, A15, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;