let AS be AffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = b or A = C )

assume A7: a <> b ; :: thesis: A = C

then A = Line (a,b) by A1, A3, A4, Lm6;

hence A = C by A2, A5, A6, A7, Lm6; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = b or A = C )

assume A7: a <> b ; :: thesis: A = C

then A = Line (a,b) by A1, A3, A4, Lm6;

hence A = C by A2, A5, A6, A7, Lm6; :: thesis: verum