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