let n be Nat; :: thesis: for Ln being Element of line_of_REAL n holds
( Ln is being_line or ex Pn being Element of REAL n st Ln = {Pn} )
let Ln be Element of line_of_REAL n; :: thesis: ( Ln is being_line or ex Pn being Element of REAL n st Ln = {Pn} )
assume A1: not Ln is being_line ; :: thesis: ex Pn being Element of REAL n st Ln = {Pn}
Ln in line_of_REAL n ;
then Ln in { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } by EUCLIDLP:def 4;
then consider x1, x2 being Element of REAL n such that
A2: Ln = Line (x1,x2) ;
x1 = x2 by A1, A2;
then Ln = {x1} by A2, Th3;
hence ex Pn being Element of REAL n st Ln = {Pn} ; :: thesis: verum