let n be Nat; :: thesis: for Ln being Element of line_of_REAL n st Ln is being_line holds
for Pn being Element of REAL n holds not Ln = {Pn}
let Ln be Element of line_of_REAL n; :: thesis: ( Ln is being_line implies for Pn being Element of REAL n holds not Ln = {Pn} )
assume A1: Ln is being_line ; :: thesis: for Pn being Element of REAL n holds not Ln = {Pn}
given x being Element of REAL n such that A2: Ln = {x} ; :: thesis: contradiction
consider x1, x2 being Element of REAL n such that
A3: x1 <> x2 and
A4: Ln = Line (x1,x2) by A1;
( x1 in {x} & x2 in {x} ) by A2, A4, EUCLID_4:9;
then ( x1 = x & x2 = x ) by TARSKI:def 1;
hence contradiction by A3; :: thesis: verum