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