let n be 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 that
A1: ( x1 in L & x2 in L ) and
A2: x1 <> x2 ; :: thesis: ( Line (x1,x2) = L & L is being_line )
A3: Line (x1,x2) c= L by A1, Th48;
L in line_of_REAL n ;
then ex y1, y2 being Element of REAL n st L = Line (y1,y2) ;
then L c= Line (x1,x2) by A1, A2, EUCLID_4:11;
then Line (x1,x2) = L by A3, XBOOLE_0:def 10;
hence ( Line (x1,x2) = L & L is being_line ) by A2; :: thesis: verum