let AS be AffinSpace; :: thesis: for A, C, D being Subset of AS st A // C & C // D holds

A // D

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

assume that

A1: A // C and

A2: C // D ; :: thesis: A // D

consider a, b, c, d being Element of AS such that

A3: a <> b and

A4: c <> d and

A5: a,b // c,d and

A6: A = Line (a,b) and

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

A8: C is being_line by A2;

A9: d in C by A7, Th14;

A10: D is being_line by A2, Th35;

then consider p, q being Element of AS such that

A11: p <> q and

A12: D = Line (p,q) ;

A13: p in D by A12, Th14;

A14: q in D by A12, Th14;

c in C by A7, Th14;

then c,d // p,q by A2, A4, A8, A10, A11, A13, A14, A9, Th37;

then a,b // p,q by A4, A5, Th4;

hence A // D by A3, A6, A11, A12, Th36; :: thesis: verum

A // D

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

assume that

A1: A // C and

A2: C // D ; :: thesis: A // D

consider a, b, c, d being Element of AS such that

A3: a <> b and

A4: c <> d and

A5: a,b // c,d and

A6: A = Line (a,b) and

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

A8: C is being_line by A2;

A9: d in C by A7, Th14;

A10: D is being_line by A2, Th35;

then consider p, q being Element of AS such that

A11: p <> q and

A12: D = Line (p,q) ;

A13: p in D by A12, Th14;

A14: q in D by A12, Th14;

c in C by A7, Th14;

then c,d // p,q by A2, A4, A8, A10, A11, A13, A14, A9, Th37;

then a,b // p,q by A4, A5, Th4;

hence A // D by A3, A6, A11, A12, Th36; :: thesis: verum