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

then A2: (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) <> {} by FINSEQ_5:47;

len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_5:42;

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

then A3: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A2, FINSEQ_6:168;

A4: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;

then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:71;

then (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A4, SPRECT_2:70, 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:72, 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:73, XXREAL_0:2;

((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 = (Cage (C,n)) /. 1 by A1, FINSEQ_5:44

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A6: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A2, FINSEQ_6:42;

( 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:40, SPRECT_2:74;

then A7: N-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A1, A5, FINSEQ_5:46, XXREAL_0:2;

A8: {(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))))) by A6, A7, A3, ENUMSET1:def 1;

then A9: 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:11;

((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_5:53;

then A10: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:42;

((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:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A11: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A11, A10, TARSKI:def 2;

then A12: 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:11;

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

then A13: 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:62;

( 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:52, SPRECT_1:13;

then (W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2 by PSCOMP_1:24;

then A14: N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n))) by SPRECT_2:57;

then card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2 by CARD_2:57;

then Segm 2 c= Segm (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) by A12, A13;

then len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2 by NAT_1:39;

then A15: 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:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A16: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) ;

then A17: ( 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:46, FINSEQ_6:61;

( 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:52, SPRECT_1:13;

then (W-max (L~ (Cage (C,n)))) `2 <= (N-max (L~ (Cage (C,n)))) `2 by PSCOMP_1:24;

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:52, SPRECT_2:57;

then A18: card {(N-min (L~ (Cage (C,n)))),(N-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 3 by A14, CARD_2:58;

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

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

then Segm 3 c= Segm (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) by A18, A9;

then A19: len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) >= 3 by NAT_1:39;

then A20: 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))))))

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

not (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) is empty by A8;

then A46: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A45, FINSEQ_6:42;

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

let n be 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:43;

then A2: (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) <> {} by FINSEQ_5:47;

len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_5:42;

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

then A3: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A2, FINSEQ_6:168;

A4: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;

then (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:71;

then (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A4, SPRECT_2:70, 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:72, 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:73, XXREAL_0:2;

((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 = (Cage (C,n)) /. 1 by A1, FINSEQ_5:44

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A6: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A2, FINSEQ_6:42;

( 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:40, SPRECT_2:74;

then A7: N-max (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A1, A5, FINSEQ_5:46, XXREAL_0:2;

A8: {(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))))) by A6, A7, A3, ENUMSET1:def 1;

then A9: 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:11;

((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_5:53;

then A10: W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:42;

((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:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A11: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A11, A10, TARSKI:def 2;

then A12: 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:11;

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

then A13: 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:62;

( 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:52, SPRECT_1:13;

then (W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2 by PSCOMP_1:24;

then A14: N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n))) by SPRECT_2:57;

then card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2 by CARD_2:57;

then Segm 2 c= Segm (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) by A12, A13;

then len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2 by NAT_1:39;

then A15: 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:54

.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

then A16: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by FINSEQ_6:168;

(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) ;

then A17: ( 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:46, FINSEQ_6:61;

( 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:52, SPRECT_1:13;

then (W-max (L~ (Cage (C,n)))) `2 <= (N-max (L~ (Cage (C,n)))) `2 by PSCOMP_1:24;

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:52, SPRECT_2:57;

then A18: card {(N-min (L~ (Cage (C,n)))),(N-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 3 by A14, CARD_2:58;

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

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

then Segm 3 c= Segm (len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) by A18, A9;

then A19: len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) >= 3 by NAT_1:39;

then A20: 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

A45: ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) /. 1 =
(Cage (C,n)) /. 1
by A1, FINSEQ_5:44
let x be object ; :: 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 A21: 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 A22: 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 A21, XBOOLE_0:def 4;

then consider i1 being Nat such that

A23: 1 <= i1 and

A24: i1 + 1 <= len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) and

A25: x1 in LSeg (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))),i1) by SPPOL_2:13;

A26: LSeg (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))),i1) = LSeg ((Cage (C,n)),i1) by A24, SPPOL_2:9;

x in L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A21, XBOOLE_0:def 4;

then consider i2 being Nat such that

A27: 1 <= i2 and

A28: i2 + 1 <= len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) and

A29: x1 in LSeg (((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))),i2) by SPPOL_2:13;

set i3 = i2 -' 1;

A30: (i2 -' 1) + 1 = i2 by A27, XREAL_1:235;

then A31: 1 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= ((i2 -' 1) + 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A27, XREAL_1:7;

A32: 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:50;

then i2 < ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A28, NAT_1:13;

then i2 - 1 < (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:19;

then A33: (i2 - 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;

i2 - 1 >= 1 - 1 by A27, XREAL_1:9;

then A34: (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by A33, XREAL_0:def 2;

A35: 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, A30, SPPOL_2:10;

A36: len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_5:42;

then i1 + 1 < ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by A24, NAT_1:13;

then i1 + 1 < ((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A31, XXREAL_0:2;

then A37: i1 + 1 <= (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by NAT_1:13;

A38: (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + 1 = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_4:21, XREAL_1:235;

(i2 -' 1) + 1 < ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A28, A30, A32, NAT_1:13;

then i2 -' 1 < (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;

then A39: (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;

then A40: ((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= len (Cage (C,n)) by NAT_1:13;

end;assume A21: 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 A22: 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 A21, XBOOLE_0:def 4;

then consider i1 being Nat such that

A23: 1 <= i1 and

A24: i1 + 1 <= len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) and

A25: x1 in LSeg (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))),i1) by SPPOL_2:13;

A26: LSeg (((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))),i1) = LSeg ((Cage (C,n)),i1) by A24, SPPOL_2:9;

x in L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) by A21, XBOOLE_0:def 4;

then consider i2 being Nat such that

A27: 1 <= i2 and

A28: i2 + 1 <= len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) and

A29: x1 in LSeg (((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))),i2) by SPPOL_2:13;

set i3 = i2 -' 1;

A30: (i2 -' 1) + 1 = i2 by A27, XREAL_1:235;

then A31: 1 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= ((i2 -' 1) + 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A27, XREAL_1:7;

A32: 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:50;

then i2 < ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A28, NAT_1:13;

then i2 - 1 < (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:19;

then A33: (i2 - 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;

i2 - 1 >= 1 - 1 by A27, XREAL_1:9;

then A34: (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by A33, XREAL_0:def 2;

A35: 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, A30, SPPOL_2:10;

A36: len ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_5:42;

then i1 + 1 < ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 by A24, NAT_1:13;

then i1 + 1 < ((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A31, XXREAL_0:2;

then A37: i1 + 1 <= (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by NAT_1:13;

A38: (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + 1 = (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, FINSEQ_4:21, XREAL_1:235;

(i2 -' 1) + 1 < ((len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 by A28, A30, A32, NAT_1:13;

then i2 -' 1 < (len (Cage (C,n))) - ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;

then A39: (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;

then A40: ((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1 <= len (Cage (C,n)) by NAT_1:13;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper 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 A23, A37, XXREAL_0:1;

end;

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 A39, GOBOARD5:def 4;

then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;

hence contradiction by A25, A29, A26, A35, XBOOLE_0:def 4; :: thesis: verum

end;then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;

hence contradiction by A25, A29, A26, A35, XBOOLE_0:def 4; :: thesis: verum

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

(i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) >= 0 + 3
by A19, A36, XREAL_1:7;

then A42: i1 + 1 < (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A41, XXREAL_0:2;

end;then A42: i1 + 1 < (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by A41, XXREAL_0:2;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper 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 A40, XXREAL_0:1;

end;

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 A42, GOBOARD5:def 4;

then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;

hence contradiction by A25, A29, A26, A35, XBOOLE_0:def 4; :: thesis: verum

end;then (LSeg ((Cage (C,n)),i1)) /\ (LSeg ((Cage (C,n)),((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))))) = {} ;

hence contradiction by A25, A29, A26, A35, XBOOLE_0:def 4; :: thesis: verum

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 A41, GOBOARD7:34, REVROT_1:30;

then x1 in {((Cage (C,n)) /. 1)} by A25, A29, A26, A35, 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 A22, TARSKI:def 2; :: thesis: verum

end;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 A41, GOBOARD7:34, REVROT_1:30;

then x1 in {((Cage (C,n)) /. 1)} by A25, A29, A26, A35, 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 A22, TARSKI:def 2; :: thesis: verum

suppose A43:
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 A34, XXREAL_0:2;

then ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

then A44: (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + (1 + 1) <= len (Cage (C,n)) by A38;

0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;

then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = i1 + 1 by A24, A36, A43, 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 A23, A38, A43, A44, TOPREAL1:def 6;

then x1 in {((Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))} by A25, A29, A26, A35, 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:38 ;

hence contradiction by A22, TARSKI:def 2; :: thesis: verum

end;then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n)) by A34, XXREAL_0:2;

then ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n)) by NAT_1:13;

then A44: (((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) -' 1) + (1 + 1) <= len (Cage (C,n)) by A38;

0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) <= (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) by XREAL_1:7;

then (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) = i1 + 1 by A24, A36, A43, 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 A23, A38, A43, A44, TOPREAL1:def 6;

then x1 in {((Cage (C,n)) /. ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))} by A25, A29, A26, A35, 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:38 ;

hence contradiction by A22, TARSKI:def 2; :: thesis: verum

.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;

not (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) is empty by A8;

then A46: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A45, FINSEQ_6:42;

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 object ; :: 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 A47: 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))))))

end;assume A47: 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 A47, TARSKI:def 2;

end;

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 A15, A20, A46, A16, 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 A15, A20, A17, XBOOLE_0:def 4; :: thesis: verum

end;