let i be Nat; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) holds
( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal )
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal )
assume A1: for j being Nat st 1 <= j & j + 1 <= len f & not (f /. j) `1 = (f /. (j + 1)) `1 holds
(f /. j) `2 = (f /. (j + 1)) `2 ; :: according to TOPREAL1:def 5 :: thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal )
set p1 = f /. i;
set p2 = f /. (i + 1);

per cases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ;

suppose A2: ( 1 <= i & i + 1 <= len f ) ; :: thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal )

A3: ( (f /. i) `2 = (f /. (i + 1)) `2 implies LSeg ((f /. i),(f /. (i + 1))) is horizontal ) by Th15;
( (f /. i) `1 = (f /. (i + 1)) `1 implies LSeg ((f /. i),(f /. (i + 1))) is vertical ) by Th16;
hence ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) by A1, A2, A3, TOPREAL1:def 3; :: thesis: verum

end;

suppose ( not 1 <= i or not i + 1 <= len f ) ; :: thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal )

then for p, q being Point of (TOP-REAL 2) st p in LSeg (f,i) & q in LSeg (f,i) holds
p `2 = q `2 by TOPREAL1:def 3;
hence ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) ; :: thesis: verum

end;

end;