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

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

end;

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

(W-min (L~ f)) `1 = (W-max (L~ f)) `1
by PSCOMP_1:29;

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

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

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

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

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

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

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

(W-min (L~ f)) `1 = (W-max (L~ f)) `1
by PSCOMP_1:29;

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

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

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

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

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

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

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

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

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

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

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

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

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

end;

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

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

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

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