let n be Nat; 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); 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); ( 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 )
; ( p1 = p2 or A = C )
assume A5:
p1 <> p2
; A = C
then
A = Line (p1,p2)
by A1, A3, Lm9;
hence
A = C
by A2, A4, A5, Lm9; verum