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

( 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