let n be Element of 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, EUCLID_4:def 2;
then ( Line x1,x2 c= A & A c= Line x1,x2 ) by A2, EUCLID_4:11, EUCLID_4:12;
hence A = Line x1,x2 by XBOOLE_0:def 10; :: thesis: verum