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 vertical holds
LSeg f,(i + 1) is horizontal
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 vertical implies LSeg f,(i + 1) is horizontal )
assume that
A1: f is special and
A2: f is alternating and
A3: 1 <= i and
A4: i + 2 <= len f and
A5: LSeg f,i is vertical ; :: thesis: LSeg f,(i + 1) is horizontal
A6: ( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11;
i + 1 <= i + 2 by XREAL_1:8;
then i + 1 <= len f by A4, XXREAL_0:2;
then LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A3, TOPREAL1:def 5;
then (f /. i) `1 = (f /. (i + 1)) `1 by A5, Th37;
then (f /. (i + 1)) `2 = (f /. (i + 2)) `2 by A1, A2, A3, A4, Th50;
then LSeg (f /. (i + 1)),(f /. (i + 2)) is horizontal by Th36;
hence LSeg f,(i + 1) is horizontal by A4, A6, TOPREAL1:def 5; :: thesis: verum