let i be Element of 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 7 :: 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 Th36;
( (f /. i) `1 = (f /. (i + 1)) `1 implies LSeg (f /. i),(f /. (i + 1)) is vertical ) by Th37;
hence ( LSeg f,i is vertical or LSeg f,i is horizontal ) by A1, A2, A3, TOPREAL1:def 5; :: 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 5;
hence ( LSeg f,i is vertical or LSeg f,i is horizontal ) by Def2; :: thesis: verum

end;

end;