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))))))
proof
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;
now :: thesis: contradiction
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 A23, A37, 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 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;
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;
now :: thesis: contradiction
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 A40, 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 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;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
A45: ((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 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))))))
per cases ( x = N-min (L~ (Cage (C,n))) or x = W-min (L~ (Cage (C,n))) ) by A47, 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 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;
end;
end;