let X be OrtAfPl; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 & M is being_line ) and
A2: ( a in A & b in A & a in M & b in M ) ; :: thesis: ( a = b or A = M )
assume A3: a <> b ; :: thesis: A = M
reconsider A' = A, M' = M as Subset of (Af X) by ANALMETR:57;
( A' is being_line & M' is being_line ) by A1, ANALMETR:58;
hence A = M by A2, A3, AFF_1:30; :: thesis: verum