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, 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; verum