let i be Nat; for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds
LSeg (f,(i + 1)) is horizontal
let f be FinSequence of the carrier of (TOP-REAL 2); ( f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical implies LSeg (f,(i + 1)) is horizontal )
assume that
A1:
( f is special & f is alternating )
and
A2:
1 <= i
and
A3:
i + 2 <= len f
and
A4:
LSeg (f,i) is vertical
; LSeg (f,(i + 1)) is horizontal
i + 1 <= i + 2
by XREAL_1:6;
then
i + 1 <= len f
by A3, XXREAL_0:2;
then
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1)))
by A2, TOPREAL1:def 3;
then
(f /. i) `1 = (f /. (i + 1)) `1
by A4, Th16;
then
(f /. (i + 1)) `2 = (f /. (i + 2)) `2
by A1, A2, A3, Th27;
then A5:
LSeg ((f /. (i + 1)),(f /. (i + 2))) is horizontal
by Th15;
( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) )
by NAT_1:11;
hence
LSeg (f,(i + 1)) is horizontal
by A3, A5, TOPREAL1:def 3; verum