let X be OrtAfPl; for a, b being Element of X
for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
let a, b be Element of X; for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
let A, M be Subset of X; ( A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b implies A = M )
assume that
A1:
A is being_line
and
A2:
M is being_line
and
A3:
a in A
and
A4:
b in A
and
A5:
a in M
and
A6:
b in M
; ( a = b or A = M )
reconsider A9 = A, M9 = M as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;
A7:
M9 is being_line
by A2, ANALMETR:43;
assume A8:
a <> b
; A = M
A9 is being_line
by A1, ANALMETR:43;
hence
A = M
by A3, A4, A5, A6, A8, A7, AFF_1:18; verum