let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); :: thesis: ( ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) implies (W-min (L~ f)) `2 < (W-max (L~ f)) `2 )
set p = W-min (L~ f);
set i = (W-min (L~ f)) .. f;
assume A1:
( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) )
; :: thesis: (W-min (L~ f)) `2 < (W-max (L~ f)) `2
A2:
len f >= 2
by REALSET1:13;
A3:
W-min (L~ f) in rng f
by SPRECT_2:47;
then A4:
(W-min (L~ f)) .. f in dom f
by FINSEQ_4:30;
A5: W-min (L~ f) =
f . ((W-min (L~ f)) .. f)
by A3, FINSEQ_4:29
.=
f /. ((W-min (L~ f)) .. f)
by A4, PARTFUN1:def 8
;
A6:
( 1 <= (W-min (L~ f)) .. f & (W-min (L~ f)) .. f <= len f )
by A4, FINSEQ_3:27;
A7:
(W-min (L~ f)) `1 = W-bound (L~ f)
by EUCLID:56;
per cases
( (W-min (L~ f)) .. f = 1 or (W-min (L~ f)) .. f = len f or ( 1 < (W-min (L~ f)) .. f & (W-min (L~ f)) .. f < len f ) )
by A6, XXREAL_0:1;
suppose that A12:
1
< (W-min (L~ f)) .. f
and A13:
(W-min (L~ f)) .. f < len f
;
:: thesis: (W-min (L~ f)) `2 < (W-max (L~ f)) `2 A14:
(((W-min (L~ f)) .. f) -' 1) + 1
= (W-min (L~ f)) .. f
by A12, XREAL_1:237;
then A15:
((W-min (L~ f)) .. f) -' 1
>= 1
by A12, NAT_1:13;
((W-min (L~ f)) .. f) -' 1
<= (W-min (L~ f)) .. f
by A14, NAT_1:11;
then
((W-min (L~ f)) .. f) -' 1
<= len f
by A13, XXREAL_0:2;
then A16:
((W-min (L~ f)) .. f) -' 1
in dom f
by A15, FINSEQ_3:27;
A17:
W-min (L~ f) in LSeg f,
(((W-min (L~ f)) .. f) -' 1)
by A5, A13, A14, A15, TOPREAL1:27;
A18:
((W-min (L~ f)) .. f) + 1
<= len f
by A13, NAT_1:13;
then A19:
W-min (L~ f) in LSeg f,
((W-min (L~ f)) .. f)
by A5, A12, TOPREAL1:27;
A20:
W-min (L~ f) <> f /. (((W-min (L~ f)) .. f) -' 1)
by A4, A5, A14, A16, GOBOARD7:31;
((W-min (L~ f)) .. f) + 1
>= 1
by NAT_1:11;
then A21:
((W-min (L~ f)) .. f) + 1
in dom f
by A18, FINSEQ_3:27;
then A22:
W-min (L~ f) <> f /. (((W-min (L~ f)) .. f) + 1)
by A3, A5, FINSEQ_4:30, GOBOARD7:31;
A23:
f /. (((W-min (L~ f)) .. f) -' 1) in LSeg f,
(((W-min (L~ f)) .. f) -' 1)
by A13, A14, A15, TOPREAL1:27;
A24:
f /. (((W-min (L~ f)) .. f) + 1) in LSeg f,
((W-min (L~ f)) .. f)
by A12, A18, TOPREAL1:27;
A25:
f /. (((W-min (L~ f)) .. f) -' 1) in L~ f
by A2, A16, GOBOARD1:16;
A26:
f /. (((W-min (L~ f)) .. f) + 1) in L~ f
by A2, A21, GOBOARD1:16;
A27:
( not
LSeg f,
(((W-min (L~ f)) .. f) -' 1) is
horizontal or not
LSeg f,
((W-min (L~ f)) .. f) is
horizontal )
proof
assume that A28:
LSeg f,
(((W-min (L~ f)) .. f) -' 1) is
horizontal
and A29:
LSeg f,
((W-min (L~ f)) .. f) is
horizontal
;
:: thesis: contradiction
A30:
((((W-min (L~ f)) .. f) -' 1) + 1) + 1
= (((W-min (L~ f)) .. f) -' 1) + (1 + 1)
;
A31:
LSeg f,
((W-min (L~ f)) .. f) = LSeg (f /. ((W-min (L~ f)) .. f)),
(f /. (((W-min (L~ f)) .. f) + 1))
by A12, A18, TOPREAL1:def 5;
A32:
LSeg f,
(((W-min (L~ f)) .. f) -' 1) = LSeg (f /. ((W-min (L~ f)) .. f)),
(f /. (((W-min (L~ f)) .. f) -' 1))
by A13, A14, A15, TOPREAL1:def 5;
A33:
(
(W-min (L~ f)) `2 = (f /. (((W-min (L~ f)) .. f) + 1)) `2 &
(W-min (L~ f)) `2 = (f /. (((W-min (L~ f)) .. f) -' 1)) `2 )
by A17, A19, A23, A24, A28, A29, SPPOL_1:def 2;
A34:
(
(W-min (L~ f)) `1 <= (f /. (((W-min (L~ f)) .. f) + 1)) `1 &
(W-min (L~ f)) `1 <= (f /. (((W-min (L~ f)) .. f) -' 1)) `1 )
by A7, A25, A26, PSCOMP_1:71;
(
(f /. (((W-min (L~ f)) .. f) + 1)) `1 <= (f /. (((W-min (L~ f)) .. f) -' 1)) `1 or
(f /. (((W-min (L~ f)) .. f) + 1)) `1 >= (f /. (((W-min (L~ f)) .. f) -' 1)) `1 )
;
then
(
f /. (((W-min (L~ f)) .. f) -' 1) in LSeg f,
((W-min (L~ f)) .. f) or
f /. (((W-min (L~ f)) .. f) + 1) in LSeg f,
(((W-min (L~ f)) .. f) -' 1) )
by A5, A31, A32, A33, A34, GOBOARD7:9;
then
(
f /. (((W-min (L~ f)) .. f) -' 1) in (LSeg f,(((W-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((W-min (L~ f)) .. f)) or
f /. (((W-min (L~ f)) .. f) + 1) in (LSeg f,(((W-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((W-min (L~ f)) .. f)) )
by A23, A24, XBOOLE_0:def 4;
then
(LSeg f,(((W-min (L~ f)) .. f) -' 1)) /\ (LSeg f,((W-min (L~ f)) .. f)) <> {(f /. ((W-min (L~ f)) .. f))}
by A5, A20, A22, TARSKI:def 1;
hence
contradiction
by A14, A15, A18, A30, TOPREAL1:def 8;
:: thesis: verum
end; now per cases
( LSeg f,(((W-min (L~ f)) .. f) -' 1) is vertical or LSeg f,((W-min (L~ f)) .. f) is vertical )
by A27, SPPOL_1:41;
suppose
LSeg f,
(((W-min (L~ f)) .. f) -' 1) is
vertical
;
:: thesis: (W-min (L~ f)) `2 < (W-max (L~ f)) `2 then A35:
(W-min (L~ f)) `1 = (f /. (((W-min (L~ f)) .. f) -' 1)) `1
by A17, A23, SPPOL_1:def 3;
then A36:
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 <> (W-min (L~ f)) `2
by A4, A5, A14, A16, GOBOARD7:31, TOPREAL3:11;
A37:
f /. (((W-min (L~ f)) .. f) -' 1) in W-most (L~ f)
by A2, A7, A16, A35, GOBOARD1:16, SPRECT_2:16;
then
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 >= (W-min (L~ f)) `2
by PSCOMP_1:88;
then A38:
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 > (W-min (L~ f)) `2
by A36, XXREAL_0:1;
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 <= (W-max (L~ f)) `2
by A37, PSCOMP_1:88;
hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
by A38, XXREAL_0:2;
:: thesis: verum end; suppose
LSeg f,
((W-min (L~ f)) .. f) is
vertical
;
:: thesis: (W-min (L~ f)) `2 < (W-max (L~ f)) `2 then A39:
(W-min (L~ f)) `1 = (f /. (((W-min (L~ f)) .. f) + 1)) `1
by A19, A24, SPPOL_1:def 3;
then A40:
(f /. (((W-min (L~ f)) .. f) + 1)) `2 <> (W-min (L~ f)) `2
by A4, A5, A21, GOBOARD7:31, TOPREAL3:11;
A41:
f /. (((W-min (L~ f)) .. f) + 1) in W-most (L~ f)
by A2, A7, A21, A39, GOBOARD1:16, SPRECT_2:16;
then
(f /. (((W-min (L~ f)) .. f) + 1)) `2 >= (W-min (L~ f)) `2
by PSCOMP_1:88;
then A42:
(f /. (((W-min (L~ f)) .. f) + 1)) `2 > (W-min (L~ f)) `2
by A40, XXREAL_0:1;
(f /. (((W-min (L~ f)) .. f) + 1)) `2 <= (W-max (L~ f)) `2
by A41, PSCOMP_1:88;
hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
by A42, XXREAL_0:2;
:: thesis: verum end; hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
;
:: thesis: verum end;