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) -: (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 Element of 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:56;
A2:
E-max (L~ (Cage C,n)) in rng (Cage C,n)
by SPRECT_2:50;
then A3:
(Cage C,n) -: (E-max (L~ (Cage C,n))) <> {}
by FINSEQ_5:50;
((Cage C,n) :- (E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n))
by FINSEQ_5:56;
then A4:
E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by FINSEQ_6:46;
((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:57
.=
(Cage C,n) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A5:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by REVROT_1:3;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) )
assume
x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
;
:: thesis: x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
hence
x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by A5, A4, TARSKI:def 2;
:: thesis: verum
end;
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:27;
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:80;
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:104;
N-max (L~ (Cage C,n)) in L~ (Cage C,n)
by SPRECT_1:13;
then
(N-max (L~ (Cage C,n))) `1 <= (E-max (L~ (Cage C,n))) `1
by A1, PSCOMP_1:71;
then A8:
N-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n))
by SPRECT_2:55;
then
card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 2
by CARD_2:76;
then
2 c= len ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by A6, A7, XBOOLE_1:1;
then
len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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:45;
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:48;
then A10:
E-max (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A3, REVROT_1:3;
((Cage C,n) -: (E-max (L~ (Cage C,n)))) /. 1 =
(Cage C,n) /. 1
by A2, FINSEQ_5:47
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A11:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A3, FINSEQ_6:46;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n)))) )
assume
x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
;
:: thesis: x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
hence
x in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A11, A10, TARSKI:def 2;
:: thesis: verum
end;
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:27;
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:80;
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:104;
((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:57
.=
(Cage C,n) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
then A14:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by REVROT_1:3;
(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:49;
card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 2
by A8, CARD_2:76;
then A16:
2 c= len ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A12, A13, XBOOLE_1:1;
then A17:
len ((Cage C,n) -: (E-max (L~ (Cage C,n)))) >= 2
by NAT_1:40;
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
set ;
:: 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
Element of
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
Element of
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:237;
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:9;
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:53;
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:21;
then A31:
(i2 - 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) < len (Cage C,n)
by XREAL_1:22;
i2 - 1
>= 1
- 1
by A25, XREAL_1:11;
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:45;
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:31, XREAL_1:237;
(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:9;
then A37:
(i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) < len (Cage C,n)
by XREAL_1:22;
then A38:
((i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) + 1
<= len (Cage C,n)
by NAT_1:13;
now 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: contradictionthen
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)))) = {}
by XBOOLE_0:def 7;
hence
contradiction
by A23, A27, A24, A33, XBOOLE_0:def 4;
:: thesis: verum end; suppose A39:
i1 = 1
;
:: thesis: contradictionA40:
(i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) >= 0 + 2
by A17, A34, XREAL_1:9;
now 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: contradictionthen A41:
i1 + 1
< (i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))
by A39;
now 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: contradictionthen
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)))) = {}
by XBOOLE_0:def 7;
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: contradictionthen
(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:36, 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:34
;
hence
contradiction
by A20, TARSKI:def 2;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; suppose A42:
(i2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n)) = 2
;
:: thesis: contradictionA43:
1
+ 2
<= len (Cage C,n)
by GOBOARD7:36, 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 8;
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:40;
then A45:
i2 -' 1
= 0
by XREAL_1:8;
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:55;
then
x1 = E-max (L~ (Cage C,n))
by FINSEQ_5:56;
hence
contradiction
by A20, TARSKI:def 2;
:: thesis: verum 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:9;
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 8;
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:41
;
hence
contradiction
by A20, TARSKI:def 2;
:: thesis: verum 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:47
.=
N-min (L~ (Cage C,n))
by JORDAN9:34
;
not (Cage C,n) -: (E-max (L~ (Cage C,n))) is empty
by A16, NAT_1:40;
then A49:
N-min (L~ (Cage C,n)) in rng ((Cage C,n) -: (E-max (L~ (Cage C,n))))
by A48, FINSEQ_6:46;
A50:
E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
by FINSEQ_6:66;
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: verumproof
let x be
set ;
:: 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)))))
end;