let i be Element of NAT ; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds
( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical )
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) implies ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) )
assume A1: ( f is special & f is alternating & 1 <= i & i + 2 <= len f ) ; :: thesis: ( ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) or ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) )
then ( LSeg (f,i) is vertical & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) implies ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) by Th55;
hence ( ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) or ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) by A1, Th41, Th56; :: thesis: verum