let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)

for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

let p1, p2 be Point of (TOP-REAL n); :: thesis: for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

let A, C be Subset of (TOP-REAL n); :: thesis: ( A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 implies A = C )

assume that

A1: A is being_line and

A2: C is being_line and

A3: ( p1 in A & p2 in A ) and

A4: ( p1 in C & p2 in C ) ; :: thesis: ( p1 = p2 or A = C )

assume A5: p1 <> p2 ; :: thesis: A = C

then A = Line (p1,p2) by A1, A3, Lm9;

hence A = C by A2, A4, A5, Lm9; :: thesis: verum

for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

let p1, p2 be Point of (TOP-REAL n); :: thesis: for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds

A = C

let A, C be Subset of (TOP-REAL n); :: thesis: ( A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 implies A = C )

assume that

A1: A is being_line and

A2: C is being_line and

A3: ( p1 in A & p2 in A ) and

A4: ( p1 in C & p2 in C ) ; :: thesis: ( p1 = p2 or A = C )

assume A5: p1 <> p2 ; :: thesis: A = C

then A = Line (p1,p2) by A1, A3, Lm9;

hence A = C by A2, A4, A5, Lm9; :: thesis: verum