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

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