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

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