let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); 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; (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))))}
XBOOLE_0:def 10 {(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 ;
TARSKI:def 3 ( 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))))))
;
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))))}
;
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 contradictionper 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 )
;
contradictionthen
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;
verum end; suppose A41:
i1 = 1
;
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 contradictionper 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))
;
contradictionthen
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;
verum end; suppose
((i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))) + 1
= len (Cage (C,n))
;
contradictionthen
(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;
verum end; end; end; hence
contradiction
;
verum end; suppose A43:
i1 + 1
= (i2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n)))
;
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;
verum end; end; end;
hence
contradiction
;
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))))))
verumproof
let x be
object ;
TARSKI:def 3 ( 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))))}
;
x in (L~ ((Cage (C,n)) -: (W-min (L~ (Cage (C,n)))))) /\ (L~ ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
end;