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

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