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 that
A1: f is special and
A2: f is alternating and
A3: 1 <= i and
A4: 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 ) )
( 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 A1, A2, A3, A4, 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, A2, A3, A4, Th41, Th56; :: thesis: verum