let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds
( Line x1,x2 = L & L is being_line )
let x1, x2 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L & x1 <> x2 holds
( Line x1,x2 = L & L is being_line )
let L be Element of line_of_REAL n; :: thesis: ( x1 in L & x2 in L & x1 <> x2 implies ( Line x1,x2 = L & L is being_line ) )
assume A1: ( x1 in L & x2 in L & x1 <> x2 ) ; :: thesis: ( Line x1,x2 = L & L is being_line )
L in line_of_REAL n ;
then consider L0 being Subset of (REAL n) such that
A2: ( L = L0 & ex y1, y2 being Element of REAL n st L0 = Line y1,y2 ) ;
consider y1, y2 being Element of REAL n such that
A3: L = Line y1,y2 by A2;
A4: L c= Line x1,x2 by A1, A3, EUCLID_4:12;
Line x1,x2 c= L by A1, Th53;
then Line x1,x2 = L by A4, XBOOLE_0:def 10;
hence ( Line x1,x2 = L & L is being_line ) by A1, EUCLID_4:def 2; :: thesis: verum