let i be Element of NAT ; :: thesis: 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 & p `2 = inf (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = inf (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )
let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = inf (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) implies ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j ) )
assume that
A1:
p `1 = ((W-bound C) + (E-bound C)) / 2
and
A2:
p `2 = inf (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1))))))
; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )
per cases
( ( L~ (Upper_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) ) or ( L~ (Upper_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) ) )
by Th9;
suppose A3:
(
L~ (Upper_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) &
L~ (Lower_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) )
;
:: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )set f =
Upper_Seq C,
(i + 1);
set G =
Gauge C,
(i + 1);
set l =
Center (Gauge C,(i + 1));
set k =
width (Gauge C,(i + 1));
A4:
(
width (Gauge C,(i + 1)) = len (Gauge C,(i + 1)) &
width (Gauge C,1) = len (Gauge C,1) )
by JORDAN8:def 1;
A5:
Upper_Seq C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by Th10;
width (Gauge C,(i + 1)) >= 4
by A4, JORDAN8:13;
then A6:
1
<= width (Gauge C,(i + 1))
by XXREAL_0:2;
then A7:
Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1))
by A4, JORDAN1B:13;
width (Gauge C,1) >= 4
by A4, JORDAN8:13;
then A8:
1
<= width (Gauge C,1)
by XXREAL_0:2;
then A9:
Center (Gauge C,1) <= len (Gauge C,1)
by A4, JORDAN1B:13;
A10:
1
<= Center (Gauge C,(i + 1))
by JORDAN1B:12;
A11:
1
<= Center (Gauge C,1)
by JORDAN1B:12;
A12:
LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) meets L~ (Upper_Seq C,(i + 1))
by A3, A4, A6, A10, JORDAN1B:13, JORDAN1B:32;
A13:
[(Center (Gauge C,(i + 1))),1] in Indices (Gauge C,(i + 1))
by A6, A7, A10, MATRIX_1:37;
[(Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))] in Indices (Gauge C,(i + 1))
by A6, A7, A10, MATRIX_1:37;
then consider n being
Element of
NAT such that A14:
( 1
<= n &
n <= width (Gauge C,(i + 1)) )
and A15:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `2 = inf (proj2 .: ((LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))))
by A5, A6, A12, A13, Th1;
take
n
;
:: thesis: ( 1 <= n & n <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n )thus
( 1
<= n &
n <= width (Gauge C,(i + 1)) )
by A14;
:: thesis: p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n
len (Gauge C,1) >= 4
by JORDAN8:13;
then A16:
1
<= len (Gauge C,1)
by XXREAL_0:2;
then A17:
p `1 =
((Gauge C,1) * (Center (Gauge C,1)),1) `1
by A1, JORDAN1A:59
.=
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `1
by A4, A14, A16, JORDAN1A:57
;
A18:
1
<= i + 1
by NAT_1:11;
(LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) = (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))
proof
thus
(LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) c= (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))
:: according to XBOOLE_0:def 10 :: thesis: (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1)))proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) or a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) )
assume A19:
a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1)))
;
:: thesis: a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))
then reconsider a1 =
a as
Point of
(TOP-REAL 2) ;
A20:
(
a1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),
((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) &
a1 in L~ (Upper_Seq C,(i + 1)) )
by A19, XBOOLE_0:def 4;
((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) `1
by A8, A9, A11, GOBOARD5:3;
then A21:
a1 `1 =
((Gauge C,1) * (Center (Gauge C,1)),1) `1
by A20, GOBOARD7:5
.=
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `1
by A4, A6, A8, JORDAN1A:57
;
then A22:
a1 `1 = ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `1
by A6, A7, A10, GOBOARD5:3;
Cage C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by JORDAN9:def 1;
then A23:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 <= S-bound (L~ (Cage C,(i + 1)))
by A4, A6, A10, JORDAN1A:43, JORDAN1B:13;
A24:
Upper_Arc (L~ (Cage C,(i + 1))) c= L~ (Cage C,(i + 1))
by JORDAN6:76;
a1 in Upper_Arc (L~ (Cage C,(i + 1)))
by A3, A19, XBOOLE_0:def 4;
then
a1 `2 >= S-bound (L~ (Cage C,(i + 1)))
by A24, PSCOMP_1:71;
then A25:
a1 `2 >= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2
by A23, XXREAL_0:2;
Cage C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by JORDAN9:def 1;
then A26:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 >= N-bound (L~ (Cage C,(i + 1)))
by A4, A6, A10, JORDAN1A:41, JORDAN1B:13;
a1 in Upper_Arc (L~ (Cage C,(i + 1)))
by A3, A19, XBOOLE_0:def 4;
then
a1 `2 <= N-bound (L~ (Cage C,(i + 1)))
by A24, PSCOMP_1:71;
then
a1 `2 <= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2
by A26, XXREAL_0:2;
then
a1 in LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))
by A21, A22, A25, GOBOARD7:8;
hence
a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))
by A20, XBOOLE_0:def 4;
:: thesis: verum
end;
thus
(LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1)))
by A4, A18, JORDAN1A:65, XBOOLE_1:26;
:: thesis: verum
end; hence
p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),
n
by A2, A3, A15, A17, TOPREAL3:11;
:: thesis: verum end; suppose A27:
(
L~ (Upper_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) &
L~ (Lower_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) )
;
:: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )set f =
Lower_Seq C,
(i + 1);
set G =
Gauge C,
(i + 1);
set l =
Center (Gauge C,(i + 1));
set k =
width (Gauge C,(i + 1));
A28:
(
width (Gauge C,(i + 1)) = len (Gauge C,(i + 1)) &
width (Gauge C,1) = len (Gauge C,1) )
by JORDAN8:def 1;
A29:
Lower_Seq C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by Th12;
width (Gauge C,(i + 1)) >= 4
by A28, JORDAN8:13;
then A30:
1
<= width (Gauge C,(i + 1))
by XXREAL_0:2;
then A31:
Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1))
by A28, JORDAN1B:13;
width (Gauge C,1) >= 4
by A28, JORDAN8:13;
then A32:
1
<= width (Gauge C,1)
by XXREAL_0:2;
then A33:
Center (Gauge C,1) <= len (Gauge C,1)
by A28, JORDAN1B:13;
A34:
1
<= Center (Gauge C,(i + 1))
by JORDAN1B:12;
A35:
1
<= Center (Gauge C,1)
by JORDAN1B:12;
A36:
LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) meets L~ (Lower_Seq C,(i + 1))
by A27, A28, A30, A34, JORDAN1B:13, JORDAN1B:32;
A37:
[(Center (Gauge C,(i + 1))),1] in Indices (Gauge C,(i + 1))
by A30, A31, A34, MATRIX_1:37;
[(Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))] in Indices (Gauge C,(i + 1))
by A30, A31, A34, MATRIX_1:37;
then consider n being
Element of
NAT such that A38:
( 1
<= n &
n <= width (Gauge C,(i + 1)) )
and A39:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `2 = inf (proj2 .: ((LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))))
by A29, A30, A36, A37, Th1;
take
n
;
:: thesis: ( 1 <= n & n <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n )thus
( 1
<= n &
n <= width (Gauge C,(i + 1)) )
by A38;
:: thesis: p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n
len (Gauge C,1) >= 4
by JORDAN8:13;
then A40:
1
<= len (Gauge C,1)
by XXREAL_0:2;
then A41:
p `1 =
((Gauge C,1) * (Center (Gauge C,1)),1) `1
by A1, JORDAN1A:59
.=
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `1
by A28, A38, A40, JORDAN1A:57
;
A42:
1
<= i + 1
by NAT_1:11;
(LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) = (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))
proof
thus
(LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) c= (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))
:: according to XBOOLE_0:def 10 :: thesis: (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1)))proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) or a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) )
assume A43:
a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1)))
;
:: thesis: a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))
then reconsider a1 =
a as
Point of
(TOP-REAL 2) ;
A44:
(
a1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),
((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) &
a1 in L~ (Lower_Seq C,(i + 1)) )
by A43, XBOOLE_0:def 4;
((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) `1
by A32, A33, A35, GOBOARD5:3;
then A45:
a1 `1 =
((Gauge C,1) * (Center (Gauge C,1)),1) `1
by A44, GOBOARD7:5
.=
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `1
by A28, A30, A32, JORDAN1A:57
;
then A46:
a1 `1 = ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `1
by A30, A31, A34, GOBOARD5:3;
Cage C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by JORDAN9:def 1;
then A47:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 <= S-bound (L~ (Cage C,(i + 1)))
by A28, A30, A34, JORDAN1A:43, JORDAN1B:13;
A48:
Upper_Arc (L~ (Cage C,(i + 1))) c= L~ (Cage C,(i + 1))
by JORDAN6:76;
a1 in Upper_Arc (L~ (Cage C,(i + 1)))
by A27, A43, XBOOLE_0:def 4;
then
a1 `2 >= S-bound (L~ (Cage C,(i + 1)))
by A48, PSCOMP_1:71;
then A49:
a1 `2 >= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2
by A47, XXREAL_0:2;
Cage C,
(i + 1) is_sequence_on Gauge C,
(i + 1)
by JORDAN9:def 1;
then A50:
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 >= N-bound (L~ (Cage C,(i + 1)))
by A28, A30, A34, JORDAN1A:41, JORDAN1B:13;
a1 in Upper_Arc (L~ (Cage C,(i + 1)))
by A27, A43, XBOOLE_0:def 4;
then
a1 `2 <= N-bound (L~ (Cage C,(i + 1)))
by A48, PSCOMP_1:71;
then
a1 `2 <= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2
by A50, XXREAL_0:2;
then
a1 in LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),
((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))
by A45, A46, A49, GOBOARD7:8;
hence
a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))
by A44, XBOOLE_0:def 4;
:: thesis: verum
end;
thus
(LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1)))
by A28, A42, JORDAN1A:65, XBOOLE_1:26;
:: thesis: verum
end; hence
p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),
n
by A2, A27, A39, A41, TOPREAL3:11;
:: thesis: verum end;