let f be non trivial special unfolded standard FinSequence of (TOP-REAL 2); :: thesis: ( ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) implies (E-min (L~ f)) `2 < (E-max (L~ f)) `2 )

set p = E-min (L~ f);

set i = (E-min (L~ f)) .. f;

assume A1: ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) ; :: thesis: (E-min (L~ f)) `2 < (E-max (L~ f)) `2

A2: len f >= 2 by NAT_D:60;

A3: (E-min (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;

A4: E-min (L~ f) in rng f by SPRECT_2:45;

then A5: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;

then A6: ( 1 <= (E-min (L~ f)) .. f & (E-min (L~ f)) .. f <= len f ) by FINSEQ_3:25;

A7: E-min (L~ f) = f . ((E-min (L~ f)) .. f) by A4, FINSEQ_4:19

.= f /. ((E-min (L~ f)) .. f) by A5, PARTFUN1:def 6 ;

set p = E-min (L~ f);

set i = (E-min (L~ f)) .. f;

assume A1: ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) ; :: thesis: (E-min (L~ f)) `2 < (E-max (L~ f)) `2

A2: len f >= 2 by NAT_D:60;

A3: (E-min (L~ f)) `1 = E-bound (L~ f) by EUCLID:52;

A4: E-min (L~ f) in rng f by SPRECT_2:45;

then A5: (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;

then A6: ( 1 <= (E-min (L~ f)) .. f & (E-min (L~ f)) .. f <= len f ) by FINSEQ_3:25;

A7: E-min (L~ f) = f . ((E-min (L~ f)) .. f) by A4, FINSEQ_4:19

.= f /. ((E-min (L~ f)) .. f) by A5, PARTFUN1:def 6 ;

per cases
( (E-min (L~ f)) .. f = 1 or (E-min (L~ f)) .. f = len f or ( 1 < (E-min (L~ f)) .. f & (E-min (L~ f)) .. f < len f ) )
by A6, XXREAL_0:1;

end;

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

(E-min (L~ f)) `1 = (E-max (L~ f)) `1
by PSCOMP_1:45;

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

(E-min (L~ f)) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:46;

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

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

(E-min (L~ f)) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:46;

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

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

(E-min (L~ f)) `1 = (E-max (L~ f)) `1
by PSCOMP_1:45;

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

(E-min (L~ f)) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:46;

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

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

(E-min (L~ f)) `2 <= (E-max (L~ f)) `2 by PSCOMP_1:46;

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

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

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

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

A14:
(((E-min (L~ f)) .. f) -' 1) + 1 = (E-min (L~ f)) .. f
by A12, XREAL_1:235;

then A15: ((E-min (L~ f)) .. f) -' 1 >= 1 by A12, NAT_1:13;

then A16: f /. (((E-min (L~ f)) .. f) -' 1) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) by A13, A14, TOPREAL1:21;

((E-min (L~ f)) .. f) -' 1 <= (E-min (L~ f)) .. f by A14, NAT_1:11;

then ((E-min (L~ f)) .. f) -' 1 <= len f by A13, XXREAL_0:2;

then A17: ((E-min (L~ f)) .. f) -' 1 in dom f by A15, FINSEQ_3:25;

then A18: f /. (((E-min (L~ f)) .. f) -' 1) in L~ f by A2, GOBOARD1:1;

A19: ((E-min (L~ f)) .. f) + 1 <= len f by A13, NAT_1:13;

then A20: f /. (((E-min (L~ f)) .. f) + 1) in LSeg (f,((E-min (L~ f)) .. f)) by A12, TOPREAL1:21;

((E-min (L~ f)) .. f) + 1 >= 1 by NAT_1:11;

then A21: ((E-min (L~ f)) .. f) + 1 in dom f by A19, FINSEQ_3:25;

then A22: f /. (((E-min (L~ f)) .. f) + 1) in L~ f by A2, GOBOARD1:1;

A23: E-min (L~ f) <> f /. (((E-min (L~ f)) .. f) + 1) by A4, A7, A21, FINSEQ_4:20, GOBOARD7:29;

A24: E-min (L~ f) in LSeg (f,((E-min (L~ f)) .. f)) by A7, A12, A19, TOPREAL1:21;

A25: E-min (L~ f) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) by A7, A13, A14, A15, TOPREAL1:21;

A26: E-min (L~ f) <> f /. (((E-min (L~ f)) .. f) -' 1) by A5, A7, A14, A17, GOBOARD7:29;

A27: ( not LSeg (f,(((E-min (L~ f)) .. f) -' 1)) is horizontal or not LSeg (f,((E-min (L~ f)) .. f)) is horizontal )

end;then A15: ((E-min (L~ f)) .. f) -' 1 >= 1 by A12, NAT_1:13;

then A16: f /. (((E-min (L~ f)) .. f) -' 1) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) by A13, A14, TOPREAL1:21;

((E-min (L~ f)) .. f) -' 1 <= (E-min (L~ f)) .. f by A14, NAT_1:11;

then ((E-min (L~ f)) .. f) -' 1 <= len f by A13, XXREAL_0:2;

then A17: ((E-min (L~ f)) .. f) -' 1 in dom f by A15, FINSEQ_3:25;

then A18: f /. (((E-min (L~ f)) .. f) -' 1) in L~ f by A2, GOBOARD1:1;

A19: ((E-min (L~ f)) .. f) + 1 <= len f by A13, NAT_1:13;

then A20: f /. (((E-min (L~ f)) .. f) + 1) in LSeg (f,((E-min (L~ f)) .. f)) by A12, TOPREAL1:21;

((E-min (L~ f)) .. f) + 1 >= 1 by NAT_1:11;

then A21: ((E-min (L~ f)) .. f) + 1 in dom f by A19, FINSEQ_3:25;

then A22: f /. (((E-min (L~ f)) .. f) + 1) in L~ f by A2, GOBOARD1:1;

A23: E-min (L~ f) <> f /. (((E-min (L~ f)) .. f) + 1) by A4, A7, A21, FINSEQ_4:20, GOBOARD7:29;

A24: E-min (L~ f) in LSeg (f,((E-min (L~ f)) .. f)) by A7, A12, A19, TOPREAL1:21;

A25: E-min (L~ f) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) by A7, A13, A14, A15, TOPREAL1:21;

A26: E-min (L~ f) <> f /. (((E-min (L~ f)) .. f) -' 1) by A5, A7, A14, A17, GOBOARD7:29;

A27: ( not LSeg (f,(((E-min (L~ f)) .. f) -' 1)) is horizontal or not LSeg (f,((E-min (L~ f)) .. f)) is horizontal )

proof

assume
( LSeg (f,(((E-min (L~ f)) .. f) -' 1)) is horizontal & LSeg (f,((E-min (L~ f)) .. f)) is horizontal )
; :: thesis: contradiction

then A28: ( (E-min (L~ f)) `2 = (f /. (((E-min (L~ f)) .. f) + 1)) `2 & (E-min (L~ f)) `2 = (f /. (((E-min (L~ f)) .. f) -' 1)) `2 ) by A25, A24, A16, A20, SPPOL_1:def 2;

A29: ( (f /. (((E-min (L~ f)) .. f) + 1)) `1 <= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 or (f /. (((E-min (L~ f)) .. f) + 1)) `1 >= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 ) ;

A30: ( (E-min (L~ f)) `1 >= (f /. (((E-min (L~ f)) .. f) + 1)) `1 & (E-min (L~ f)) `1 >= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 ) by A3, A18, A22, PSCOMP_1:24;

( LSeg (f,((E-min (L~ f)) .. f)) = LSeg ((f /. ((E-min (L~ f)) .. f)),(f /. (((E-min (L~ f)) .. f) + 1))) & LSeg (f,(((E-min (L~ f)) .. f) -' 1)) = LSeg ((f /. ((E-min (L~ f)) .. f)),(f /. (((E-min (L~ f)) .. f) -' 1))) ) by A12, A13, A14, A15, A19, TOPREAL1:def 3;

then ( f /. (((E-min (L~ f)) .. f) -' 1) in LSeg (f,((E-min (L~ f)) .. f)) or f /. (((E-min (L~ f)) .. f) + 1) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) ) by A7, A28, A30, A29, GOBOARD7:8;

then ( f /. (((E-min (L~ f)) .. f) -' 1) in (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) or f /. (((E-min (L~ f)) .. f) + 1) in (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) ) by A16, A20, XBOOLE_0:def 4;

then ( ((((E-min (L~ f)) .. f) -' 1) + 1) + 1 = (((E-min (L~ f)) .. f) -' 1) + (1 + 1) & (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) <> {(f /. ((E-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: ( (E-min (L~ f)) `2 = (f /. (((E-min (L~ f)) .. f) + 1)) `2 & (E-min (L~ f)) `2 = (f /. (((E-min (L~ f)) .. f) -' 1)) `2 ) by A25, A24, A16, A20, SPPOL_1:def 2;

A29: ( (f /. (((E-min (L~ f)) .. f) + 1)) `1 <= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 or (f /. (((E-min (L~ f)) .. f) + 1)) `1 >= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 ) ;

A30: ( (E-min (L~ f)) `1 >= (f /. (((E-min (L~ f)) .. f) + 1)) `1 & (E-min (L~ f)) `1 >= (f /. (((E-min (L~ f)) .. f) -' 1)) `1 ) by A3, A18, A22, PSCOMP_1:24;

( LSeg (f,((E-min (L~ f)) .. f)) = LSeg ((f /. ((E-min (L~ f)) .. f)),(f /. (((E-min (L~ f)) .. f) + 1))) & LSeg (f,(((E-min (L~ f)) .. f) -' 1)) = LSeg ((f /. ((E-min (L~ f)) .. f)),(f /. (((E-min (L~ f)) .. f) -' 1))) ) by A12, A13, A14, A15, A19, TOPREAL1:def 3;

then ( f /. (((E-min (L~ f)) .. f) -' 1) in LSeg (f,((E-min (L~ f)) .. f)) or f /. (((E-min (L~ f)) .. f) + 1) in LSeg (f,(((E-min (L~ f)) .. f) -' 1)) ) by A7, A28, A30, A29, GOBOARD7:8;

then ( f /. (((E-min (L~ f)) .. f) -' 1) in (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) or f /. (((E-min (L~ f)) .. f) + 1) in (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) ) by A16, A20, XBOOLE_0:def 4;

then ( ((((E-min (L~ f)) .. f) -' 1) + 1) + 1 = (((E-min (L~ f)) .. f) -' 1) + (1 + 1) & (LSeg (f,(((E-min (L~ f)) .. f) -' 1))) /\ (LSeg (f,((E-min (L~ f)) .. f))) <> {(f /. ((E-min (L~ f)) .. f))} ) by A7, A26, A23, TARSKI:def 1;

hence contradiction by A14, A15, A19, TOPREAL1:def 6; :: thesis: verum

now :: thesis: (E-min (L~ f)) `2 < (E-max (L~ f)) `2 end;

hence
(E-min (L~ f)) `2 < (E-max (L~ f)) `2
; :: thesis: verumper cases
( LSeg (f,(((E-min (L~ f)) .. f) -' 1)) is vertical or LSeg (f,((E-min (L~ f)) .. f)) is vertical )
by A27, SPPOL_1:19;

end;

suppose
LSeg (f,(((E-min (L~ f)) .. f) -' 1)) is vertical
; :: thesis: (E-min (L~ f)) `2 < (E-max (L~ f)) `2

then A31:
(E-min (L~ f)) `1 = (f /. (((E-min (L~ f)) .. f) -' 1)) `1
by A25, A16, SPPOL_1:def 3;

then A32: f /. (((E-min (L~ f)) .. f) -' 1) in E-most (L~ f) by A2, A3, A17, GOBOARD1:1, SPRECT_2:13;

then A33: (f /. (((E-min (L~ f)) .. f) -' 1)) `2 >= (E-min (L~ f)) `2 by PSCOMP_1:47;

(f /. (((E-min (L~ f)) .. f) -' 1)) `2 <> (E-min (L~ f)) `2 by A5, A7, A14, A17, A31, GOBOARD7:29, TOPREAL3:6;

then A34: (f /. (((E-min (L~ f)) .. f) -' 1)) `2 > (E-min (L~ f)) `2 by A33, XXREAL_0:1;

(f /. (((E-min (L~ f)) .. f) -' 1)) `2 <= (E-max (L~ f)) `2 by A32, PSCOMP_1:47;

hence (E-min (L~ f)) `2 < (E-max (L~ f)) `2 by A34, XXREAL_0:2; :: thesis: verum

end;then A32: f /. (((E-min (L~ f)) .. f) -' 1) in E-most (L~ f) by A2, A3, A17, GOBOARD1:1, SPRECT_2:13;

then A33: (f /. (((E-min (L~ f)) .. f) -' 1)) `2 >= (E-min (L~ f)) `2 by PSCOMP_1:47;

(f /. (((E-min (L~ f)) .. f) -' 1)) `2 <> (E-min (L~ f)) `2 by A5, A7, A14, A17, A31, GOBOARD7:29, TOPREAL3:6;

then A34: (f /. (((E-min (L~ f)) .. f) -' 1)) `2 > (E-min (L~ f)) `2 by A33, XXREAL_0:1;

(f /. (((E-min (L~ f)) .. f) -' 1)) `2 <= (E-max (L~ f)) `2 by A32, PSCOMP_1:47;

hence (E-min (L~ f)) `2 < (E-max (L~ f)) `2 by A34, XXREAL_0:2; :: thesis: verum

suppose
LSeg (f,((E-min (L~ f)) .. f)) is vertical
; :: thesis: (E-min (L~ f)) `2 < (E-max (L~ f)) `2

then A35:
(E-min (L~ f)) `1 = (f /. (((E-min (L~ f)) .. f) + 1)) `1
by A24, A20, SPPOL_1:def 3;

then A36: f /. (((E-min (L~ f)) .. f) + 1) in E-most (L~ f) by A2, A3, A21, GOBOARD1:1, SPRECT_2:13;

then A37: (f /. (((E-min (L~ f)) .. f) + 1)) `2 >= (E-min (L~ f)) `2 by PSCOMP_1:47;

(f /. (((E-min (L~ f)) .. f) + 1)) `2 <> (E-min (L~ f)) `2 by A5, A7, A21, A35, GOBOARD7:29, TOPREAL3:6;

then A38: (f /. (((E-min (L~ f)) .. f) + 1)) `2 > (E-min (L~ f)) `2 by A37, XXREAL_0:1;

(f /. (((E-min (L~ f)) .. f) + 1)) `2 <= (E-max (L~ f)) `2 by A36, PSCOMP_1:47;

hence (E-min (L~ f)) `2 < (E-max (L~ f)) `2 by A38, XXREAL_0:2; :: thesis: verum

end;then A36: f /. (((E-min (L~ f)) .. f) + 1) in E-most (L~ f) by A2, A3, A21, GOBOARD1:1, SPRECT_2:13;

then A37: (f /. (((E-min (L~ f)) .. f) + 1)) `2 >= (E-min (L~ f)) `2 by PSCOMP_1:47;

(f /. (((E-min (L~ f)) .. f) + 1)) `2 <> (E-min (L~ f)) `2 by A5, A7, A21, A35, GOBOARD7:29, TOPREAL3:6;

then A38: (f /. (((E-min (L~ f)) .. f) + 1)) `2 > (E-min (L~ f)) `2 by A37, XXREAL_0:1;

(f /. (((E-min (L~ f)) .. f) + 1)) `2 <= (E-max (L~ f)) `2 by A36, PSCOMP_1:47;

hence (E-min (L~ f)) `2 < (E-max (L~ f)) `2 by A38, XXREAL_0:2; :: thesis: verum