let i, k be Nat; for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let p be Point of (TOP-REAL 2); ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) implies ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) )
assume that
A1:
p `1 = ((W-bound C) + (E-bound C)) / 2
and
A2:
i > 0
and
A3:
1 <= k
and
A4:
k <= width (Gauge (C,i))
and
A5:
(Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i)))
and
A6:
p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i))))))
; ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
set f = Lower_Seq (C,i);
set G = Gauge (C,i);
A7:
Center (Gauge (C,i)) <= len (Gauge (C,i))
by JORDAN1B:13;
4 <= len (Gauge (C,i))
by JORDAN8:10;
then A8:
1 <= len (Gauge (C,i))
by XXREAL_0:2;
4 <= len (Gauge (C,1))
by JORDAN8:10;
then
1 <= len (Gauge (C,1))
by XXREAL_0:2;
then A9:
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1
by A2, A8, JORDAN1A:36;
A10:
( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) )
by JORDAN1B:11, JORDAN1B:13;
A11:
1 <= Center (Gauge (C,i))
by JORDAN1B:11;
then A12:
((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1
by A3, A4, A7, GOBOARD5:2;
0 + 1 <= i
by A2, NAT_1:13;
then A13:
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2
by A11, A7, A10, JORDAN1A:43;
A14:
(LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
proof
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) or a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) )
assume A15:
a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
;
a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
then reconsider q =
a as
Point of
(TOP-REAL 2) ;
A16:
a in LSeg (
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),
((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by A15, XBOOLE_0:def 4;
A17:
a in L~ (Lower_Seq (C,i))
by A15, XBOOLE_0:def 4;
then
q in (L~ (Lower_Seq (C,i))) \/ (L~ (Upper_Seq (C,i)))
by XBOOLE_0:def 3;
then
q in L~ (Cage (C,i))
by JORDAN1E:13;
then
S-bound (L~ (Cage (C,i))) <= q `2
by PSCOMP_1:24;
then A18:
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2
by A7, JORDAN1A:72, JORDAN1B:11;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2
by A3, A4, A11, A7, JORDAN1A:19;
then
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2
by A13, XXREAL_0:2;
then A19:
q `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2
by A16, TOPREAL1:4;
q `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `1
by A9, A12, A16, GOBOARD7:5;
then
q in LSeg (
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),
((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by A12, A19, A18, GOBOARD7:7;
hence
a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
by A17, XBOOLE_0:def 4;
verum
end;
A20:
(Gauge (C,i)) * ((Center (Gauge (C,i))),k) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by RLTOPSP1:68;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2
by A3, A4, A11, A7, JORDAN1A:19;
then
(Gauge (C,i)) * ((Center (Gauge (C,i))),1) in LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by A9, A12, A13, GOBOARD7:7;
then
LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k))) c= LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))
by A20, TOPREAL1:6;
then
(LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) c= (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
by XBOOLE_1:27;
then
(LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) = (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
by A14, XBOOLE_0:def 10;
then A21:
upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))))) = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i))))))
by A2, JORDAN1G:56;
A22:
( Lower_Seq (C,i) is_sequence_on Gauge (C,i) & Upper_Arc (L~ (Cage (C,i))) c= L~ (Cage (C,i)) )
by JORDAN1F:12, JORDAN6:61;
len (Gauge (C,i)) >= 4
by JORDAN8:10;
then
width (Gauge (C,i)) >= 4
by JORDAN8:def 1;
then
1 <= width (Gauge (C,i))
by XXREAL_0:2;
then A23:
[(Center (Gauge (C,i))),1] in Indices (Gauge (C,i))
by A11, A7, MATRIX_0:30;
[(Center (Gauge (C,i))),k] in Indices (Gauge (C,i))
by A3, A4, A11, A7, MATRIX_0:30;
then consider n being Nat such that
A24:
1 <= n
and
A25:
n <= k
and
A26:
((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))))
by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:46;
take
n
; ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus
1 <= n
by A24; ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus
n <= width (Gauge (C,i))
by A4, A25, XXREAL_0:2; p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)
then
p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1
by A1, A2, A24, JORDAN1G:35;
hence
p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)
by A6, A26, A21, TOPREAL3:6; verum