let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); :: thesis: ( ( ( 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) ) ) ; :: thesis: (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 ;

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) ) ) ; :: thesis: (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;

end;

suppose A8:
(S-min (L~ f)) .. f = 1
; :: thesis: (S-min (L~ f)) `1 < (S-max (L~ f)) `1

(S-min (L~ f)) `2 = (S-max (L~ f)) `2
by PSCOMP_1:53;

then A9: (S-min (L~ f)) `1 <> (S-max (L~ f)) `1 by A1, A7, A8, TOPREAL3:6;

(S-min (L~ f)) `1 <= (S-max (L~ f)) `1 by PSCOMP_1:54;

hence (S-min (L~ f)) `1 < (S-max (L~ f)) `1 by A9, XXREAL_0:1; :: thesis: verum

end;then A9: (S-min (L~ f)) `1 <> (S-max (L~ f)) `1 by A1, A7, A8, TOPREAL3:6;

(S-min (L~ f)) `1 <= (S-max (L~ f)) `1 by PSCOMP_1:54;

hence (S-min (L~ f)) `1 < (S-max (L~ f)) `1 by A9, XXREAL_0:1; :: thesis: verum

suppose A10:
(S-min (L~ f)) .. f = len f
; :: thesis: (S-min (L~ f)) `1 < (S-max (L~ f)) `1

(S-min (L~ f)) `2 = (S-max (L~ f)) `2
by PSCOMP_1:53;

then A11: (S-min (L~ f)) `1 <> (S-max (L~ f)) `1 by A1, A7, A10, TOPREAL3:6;

(S-min (L~ f)) `1 <= (S-max (L~ f)) `1 by PSCOMP_1:54;

hence (S-min (L~ f)) `1 < (S-max (L~ f)) `1 by A11, XXREAL_0:1; :: thesis: verum

end;then A11: (S-min (L~ f)) `1 <> (S-max (L~ f)) `1 by A1, A7, A10, TOPREAL3:6;

(S-min (L~ f)) `1 <= (S-max (L~ f)) `1 by PSCOMP_1:54;

hence (S-min (L~ f)) `1 < (S-max (L~ f)) `1 by A11, XXREAL_0:1; :: thesis: verum

suppose that A12:
1 < (S-min (L~ f)) .. f
and

A13: (S-min (L~ f)) .. f < len f ; :: thesis: (S-min (L~ f)) `1 < (S-max (L~ f)) `1

A13: (S-min (L~ f)) .. f < len f ; :: thesis: (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 )

end;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 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: (S-min (L~ f)) `1 < (S-max (L~ f)) `1 end;

hence
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
; :: thesis: verumper 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;

end;

suppose
LSeg (f,(((S-min (L~ f)) .. f) -' 1)) is horizontal
; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum

suppose
LSeg (f,((S-min (L~ f)) .. f)) is horizontal
; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum