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

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

a,b // C

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

a,b // C

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

assume that

A1: a,b // A and

A2: A // C ; :: thesis: a,b // C

consider p, q, c, d being Element of AS such that

A3: p <> q and

A4: c <> d and

A5: p,q // c,d and

A6: A = Line (p,q) and

A7: C = Line (c,d) by A2, Th36;

A8: q in A by A6, Th14;

A9: A is being_line by A2;

p in A by A6, Th14;

then a,b // p,q by A1, A3, A8, A9, Th26;

then a,b // c,d by A3, A5, Th4;

hence a,b // C by A4, A7; :: thesis: verum

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

a,b // C

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

a,b // C

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

assume that

A1: a,b // A and

A2: A // C ; :: thesis: a,b // C

consider p, q, c, d being Element of AS such that

A3: p <> q and

A4: c <> d and

A5: p,q // c,d and

A6: A = Line (p,q) and

A7: C = Line (c,d) by A2, Th36;

A8: q in A by A6, Th14;

A9: A is being_line by A2;

p in A by A6, Th14;

then a,b // p,q by A1, A3, A8, A9, Th26;

then a,b // c,d by A3, A5, Th4;

hence a,b // C by A4, A7; :: thesis: verum