let AS be AffinSpace; for A, C, D being Subset of AS st A // C & C // D holds
A // D
let A, C, D be Subset of AS; ( A // C & C // D implies A // D )
assume that
A1:
A // C
and
A2:
C // D
; 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, Th51;
A8:
C is being_line
by A2, Th50;
A9:
d in C
by A7, Th26;
A10:
D is being_line
by A2, Th50;
then consider p, q being Element of AS such that
A11:
p <> q
and
A12:
D = Line (p,q)
by Def3;
A13:
p in D
by A12, Th26;
A14:
q in D
by A12, Th26;
c in C
by A7, Th26;
then
c,d // p,q
by A2, A4, A8, A10, A11, A13, A14, A9, Th52;
then
a,b // p,q
by A4, A5, Th14;
hence
A // D
by A3, A6, A11, A12, Th51; verum