let AS be AffinSpace; for a, b being Element of AS
for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds
A = C
let a, b be Element of AS; for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds
A = C
let A, C be Subset of AS; ( A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b implies A = C )
assume that
A1:
A is being_line
and
A2:
C is being_line
and
A3:
a in A
and
A4:
b in A
and
A5:
a in C
and
A6:
b in C
; ( a = b or A = C )
assume A7:
a <> b
; A = C
then
A = Line (a,b)
by A1, A3, A4, Lm6;
hence
A = C
by A2, A5, A6, A7, Lm6; verum