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
A3: ex y1, y2 being Element of REAL n st
( y1 <> y2 & A = Line y1,y2 ) by A1, Def2;
then A4: Line x1,x2 c= A by A2, Th11;
A c= Line x1,x2 by A2, A3, Th12;
hence A = Line x1,x2 by A4, XBOOLE_0:def 10; :: thesis: verum