let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); ( ( ( 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) ) )
; (W-min (L~ f)) `2 < (W-max (L~ f)) `2
A2:
len f >= 2
by NAT_D:60;
A3:
(W-min (L~ f)) `1 = W-bound (L~ f)
by EUCLID:52;
A4:
W-min (L~ f) in rng f
by SPRECT_2:43;
then A5:
(W-min (L~ f)) .. f in dom f
by FINSEQ_4:20;
then A6:
( 1 <= (W-min (L~ f)) .. f & (W-min (L~ f)) .. f <= len f )
by FINSEQ_3:25;
A7: W-min (L~ f) =
f . ((W-min (L~ f)) .. f)
by A4, FINSEQ_4:19
.=
f /. ((W-min (L~ f)) .. f)
by A5, PARTFUN1:def 6
;
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
;
(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:235;
then A15:
((W-min (L~ f)) .. f) -' 1
>= 1
by A12, NAT_1:13;
then A16:
f /. (((W-min (L~ f)) .. f) -' 1) in LSeg (
f,
(((W-min (L~ f)) .. f) -' 1))
by A13, A14, TOPREAL1:21;
((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 A17:
((W-min (L~ f)) .. f) -' 1
in dom f
by A15, FINSEQ_3:25;
then A18:
f /. (((W-min (L~ f)) .. f) -' 1) in L~ f
by A2, GOBOARD1:1;
A19:
((W-min (L~ f)) .. f) + 1
<= len f
by A13, NAT_1:13;
then A20:
f /. (((W-min (L~ f)) .. f) + 1) in LSeg (
f,
((W-min (L~ f)) .. f))
by A12, TOPREAL1:21;
((W-min (L~ f)) .. f) + 1
>= 1
by NAT_1:11;
then A21:
((W-min (L~ f)) .. f) + 1
in dom f
by A19, FINSEQ_3:25;
then A22:
f /. (((W-min (L~ f)) .. f) + 1) in L~ f
by A2, GOBOARD1:1;
A23:
W-min (L~ f) <> f /. (((W-min (L~ f)) .. f) + 1)
by A4, A7, A21, FINSEQ_4:20, GOBOARD7:29;
A24:
W-min (L~ f) in LSeg (
f,
((W-min (L~ f)) .. f))
by A7, A12, A19, TOPREAL1:21;
A25:
W-min (L~ f) in LSeg (
f,
(((W-min (L~ f)) .. f) -' 1))
by A7, A13, A14, A15, TOPREAL1:21;
A26:
W-min (L~ f) <> f /. (((W-min (L~ f)) .. f) -' 1)
by A5, A7, A14, A17, GOBOARD7:29;
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
(
LSeg (
f,
(((W-min (L~ f)) .. f) -' 1)) is
horizontal &
LSeg (
f,
((W-min (L~ f)) .. f)) is
horizontal )
;
contradiction
then A28:
(
(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 A25, A24, A16, A20, SPPOL_1:def 2;
A29:
(
(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 )
;
A30:
(
(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 A3, A18, A22, PSCOMP_1:24;
(
LSeg (
f,
((W-min (L~ f)) .. f))
= LSeg (
(f /. ((W-min (L~ f)) .. f)),
(f /. (((W-min (L~ f)) .. f) + 1))) &
LSeg (
f,
(((W-min (L~ f)) .. f) -' 1))
= LSeg (
(f /. ((W-min (L~ f)) .. f)),
(f /. (((W-min (L~ f)) .. f) -' 1))) )
by A12, A13, A14, A15, A19, TOPREAL1:def 3;
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 A7, A28, A30, A29, GOBOARD7:8;
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 A16, A20, XBOOLE_0:def 4;
then
(
((((W-min (L~ f)) .. f) -' 1) + 1) + 1
= (((W-min (L~ f)) .. f) -' 1) + (1 + 1) &
(LSeg (f,(((W-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((W-min (L~ f)) .. f))) <> {(f /. ((W-min (L~ f)) .. f))} )
by A7, A26, A23, TARSKI:def 1;
hence
contradiction
by A14, A15, A19, TOPREAL1:def 6;
verum
end; now (W-min (L~ f)) `2 < (W-max (L~ f)) `2 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:19;
suppose
LSeg (
f,
(((W-min (L~ f)) .. f) -' 1)) is
vertical
;
(W-min (L~ f)) `2 < (W-max (L~ f)) `2 then A31:
(W-min (L~ f)) `1 = (f /. (((W-min (L~ f)) .. f) -' 1)) `1
by A25, A16, SPPOL_1:def 3;
then A32:
f /. (((W-min (L~ f)) .. f) -' 1) in W-most (L~ f)
by A2, A3, A17, GOBOARD1:1, SPRECT_2:12;
then A33:
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 >= (W-min (L~ f)) `2
by PSCOMP_1:31;
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 <> (W-min (L~ f)) `2
by A5, A7, A14, A17, A31, GOBOARD7:29, TOPREAL3:6;
then A34:
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 > (W-min (L~ f)) `2
by A33, XXREAL_0:1;
(f /. (((W-min (L~ f)) .. f) -' 1)) `2 <= (W-max (L~ f)) `2
by A32, PSCOMP_1:31;
hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
by A34, XXREAL_0:2;
verum end; suppose
LSeg (
f,
((W-min (L~ f)) .. f)) is
vertical
;
(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 A24, A20, SPPOL_1:def 3;
then A36:
f /. (((W-min (L~ f)) .. f) + 1) in W-most (L~ f)
by A2, A3, A21, GOBOARD1:1, SPRECT_2:12;
then A37:
(f /. (((W-min (L~ f)) .. f) + 1)) `2 >= (W-min (L~ f)) `2
by PSCOMP_1:31;
(f /. (((W-min (L~ f)) .. f) + 1)) `2 <> (W-min (L~ f)) `2
by A5, A7, A21, A35, GOBOARD7:29, TOPREAL3:6;
then A38:
(f /. (((W-min (L~ f)) .. f) + 1)) `2 > (W-min (L~ f)) `2
by A37, XXREAL_0:1;
(f /. (((W-min (L~ f)) .. f) + 1)) `2 <= (W-max (L~ f)) `2
by A36, PSCOMP_1:31;
hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
by A38, XXREAL_0:2;
verum end; end; end; hence
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
;
verum end; end;