let AS be AffinSpace; :: thesis: for a, b being Element of AS

for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds

A // C

let a, b be Element of AS; :: thesis: for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds

A // C

let A, C be Subset of AS; :: thesis: ( a,b // A & a,b // C & a <> b implies A // C )

assume that

A1: a,b // A and

A2: a,b // C and

A3: a <> b ; :: thesis: A // C

A4: C is being_line by A2;

then consider p, q being Element of AS such that

A5: p <> q and

A6: p in C and

A7: q in C and

A8: a,b // p,q by A2, Th29;

A9: A is being_line by A1;

then consider c, d being Element of AS such that

A10: c <> d and

A11: c in A and

A12: d in A and

A13: a,b // c,d by A1, Th29;

c,d // p,q by A3, A13, A8, Th4;

hence A // C by A9, A4, A10, A11, A12, A5, A6, A7, Th37; :: thesis: verum

for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds

A // C

let a, b be Element of AS; :: thesis: for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds

A // C

let A, C be Subset of AS; :: thesis: ( a,b // A & a,b // C & a <> b implies A // C )

assume that

A1: a,b // A and

A2: a,b // C and

A3: a <> b ; :: thesis: A // C

A4: C is being_line by A2;

then consider p, q being Element of AS such that

A5: p <> q and

A6: p in C and

A7: q in C and

A8: a,b // p,q by A2, Th29;

A9: A is being_line by A1;

then consider c, d being Element of AS such that

A10: c <> d and

A11: c in A and

A12: d in A and

A13: a,b // c,d by A1, Th29;

c,d // p,q by A3, A13, A8, Th4;

hence A // C by A9, A4, A10, A11, A12, A5, A6, A7, Th37; :: thesis: verum