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: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, REVROT_1:3;
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;
{(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:11;
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1 = W-min (L~ (Cage (C,n))) by FINSEQ_5:53;
then A9: 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 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: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 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: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 A13: 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 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:39;
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:54
.= (Cage (C,n)) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
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: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 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: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 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:39;
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:235;
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:7;
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:50;
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:19;
then A32: (i2 - 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;
i2 - 1 >= 1 - 1 by A26, XREAL_1:9;
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:42;
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:21, XREAL_1:235;
(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:7;
then A38: (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) < len (Cage (C,n)) by XREAL_1:20;
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:7;
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:34, 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:32 ;
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:7;
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 6;
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:38 ;
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:44
.= N-min (L~ (Cage (C,n))) by JORDAN9:32 ;
not (Cage (C,n)) -: (W-min (L~ (Cage (C,n)))) is empty by A17, A8, NAT_1:39;
then A45: N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) -: (W-min (L~ (Cage (C,n))))) by A44, 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 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;