let AS be AffinSpace; :: thesis: for A, C being Subset of AS st A // C holds
C // A
let A, C be Subset of AS; :: thesis: ( A // C implies C // A )
assume A // C ; :: thesis: 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; :: thesis: verum