let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A in LSeg (B,C) implies A in Line (B,C) )
assume A in LSeg (B,C) ; :: thesis: A in Line (B,C)
then consider lambda being Real such that
A1: ( A = ((1 - lambda) * B) + (lambda * C) & 0 <= lambda & lambda <= 1 ) ;
thus A in Line (B,C) by A1; :: thesis: verum