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