let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,1) holds

Index (p,f) = 1

let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (f,1) implies Index (p,f) = 1 )

assume A1: p in LSeg (f,1) ; :: thesis: Index (p,f) = 1

then A2: Index (p,f) <= 1 by Th7;

LSeg (f,1) c= L~ f by TOPREAL3:19;

then Index (p,f) >= 1 by A1, Th8;

hence Index (p,f) = 1 by A2, XXREAL_0:1; :: thesis: verum

Index (p,f) = 1

let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (f,1) implies Index (p,f) = 1 )

assume A1: p in LSeg (f,1) ; :: thesis: Index (p,f) = 1

then A2: Index (p,f) <= 1 by Th7;

LSeg (f,1) c= L~ f by TOPREAL3:19;

then Index (p,f) >= 1 by A1, Th8;

hence Index (p,f) = 1 by A2, XXREAL_0:1; :: thesis: verum