let n be Nat; :: thesis: for A, C being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let A, C be Subset of (REAL n); :: thesis: for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let x1, x2 be Element of REAL n; :: thesis: ( A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 implies A = C )
assume that
A1: A is being_line and
A2: C is being_line and
A3: ( x1 in A & x2 in A ) and
A4: ( x1 in C & x2 in C ) ; :: thesis: ( x1 = x2 or A = C )
assume A5: x1 <> x2 ; :: thesis: A = C
then A = Line (x1,x2) by A1, A3, Lm3;
hence A = C by A2, A4, A5, Lm3; :: thesis: verum