let n be Nat; :: thesis: for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line (x1,x2)
let A be Subset of (REAL n); :: thesis: for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line (x1,x2)
let x1, x2 be Element of REAL n; :: thesis: ( A is being_line & x1 in A & x2 in A & x1 <> x2 implies A = Line (x1,x2) )
assume that
A1: A is being_line and
A2: ( x1 in A & x2 in A & x1 <> x2 ) ; :: thesis: A = Line (x1,x2)
ex y1, y2 being Element of REAL n st
( y1 <> y2 & A = Line (y1,y2) ) by A1;
then ( Line (x1,x2) c= A & A c= Line (x1,x2) ) by A2, EUCLID_4:10, EUCLID_4:11;
hence A = Line (x1,x2) by XBOOLE_0:def 10; :: thesis: verum