let i be 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 & LSeg (f,i) is horizontal holds
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 & LSeg (f,i) is horizontal implies LSeg (f,(i + 1)) is vertical )
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 horizontal ; :: thesis: LSeg (f,(i + 1)) is vertical
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) `2 = (f /. (i + 1)) `2 by A4, Th15;
then (f /. (i + 1)) `1 = (f /. (i + 2)) `1 by A1, A2, A3, Th28;
then A5: LSeg ((f /. (i + 1)),(f /. (i + 2))) is vertical by Th16;
( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11;
hence LSeg (f,(i + 1)) is vertical by A3, A5, TOPREAL1:def 3; :: thesis: verum