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 & 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:8;
then i + 1 <= len f by A3, XXREAL_0:2;
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, TOPREAL1:def 5;
then (f /. i) `2 = (f /. (i + 1)) `2 by A4, Th36;
then (f /. (i + 1)) `1 = (f /. (i + 2)) `1 by A1, A2, A3, Th51;
then A5: LSeg (f /. (i + 1)),(f /. (i + 2)) is vertical by Th37;
( 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 5; :: thesis: verum