let AS be AffinSpace; for A, C being Subset of AS st A // C holds
C // A
let A, C be Subset of AS; ( A // C implies C // A )
assume
A // C
; C // A
then consider a, b, c, d being Element of AS such that
A1:
a <> b
and
A2:
c <> d
and
A3:
a,b // c,d
and
A4:
A = Line (a,b)
and
A5:
C = Line (c,d)
by Th36;
c,d // a,b
by A3, Th3;
hence
C // A
by A1, A2, A4, A5, Th36; verum