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