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 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 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 ; :: thesis: A = M

A9 is being_line by A1, ANALMETR:43;

hence A = M by A3, A4, A5, A6, A8, A7, AFF_1:18; :: thesis: verum

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 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 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 ; :: thesis: A = M

A9 is being_line by A1, ANALMETR:43;

hence A = M by A3, A4, A5, A6, A8, A7, AFF_1:18; :: thesis: verum