let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d
let a, b, c, d be Element of AS; :: thesis: for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds
a,b // c,d
let A, C be Subset of AS; :: thesis: ( a in A & b in A & c in C & d in C & A // C implies a,b // c,d )
assume that
A1: a in A and
A2: b in A and
A3: c in C and
A4: d in C and
A5: A // C ; :: thesis: a,b // c,d

now :: thesis: ( a <> b & c <> d implies a,b // c,d )

A6: C is being_line by A5, Th35;
assume that
A7: a <> b and
A8: c <> d ; :: thesis: a,b // c,d
A is being_line by A5;
hence a,b // c,d by A1, A2, A3, A4, A5, A7, A8, A6, Th37; :: thesis: verum

end;

hence a,b // c,d by Th2; :: thesis: verum