let X be OrtAfPl; :: thesis: for a, b being Element of
for A, M being Subset of 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 ; :: thesis: for A, M being Subset of 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 ; :: 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 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 ; :: thesis: ( a = b or A = M )
reconsider A' = A, M' = M as Subset of by ANALMETR:57;
A7: M' is being_line by A2, ANALMETR:58;
assume A8: a <> b ; :: thesis: A = M
A' is being_line by A1, ANALMETR:58;
hence A = M by A3, A4, A5, A6, A8, A7, AFF_1:30; :: thesis: verum