let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A, C being Subset of AS st ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C holds
d in C
let a, b, c, d be Element of AS; :: thesis: for A, C being Subset of AS st ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C holds
d in C
let A, C be Subset of AS; :: thesis: ( ( A // C or C // A ) & a <> b & ( a,b // c,d or c,d // a,b ) & a in A & b in A & c in C implies d in C )
assume that
A1: ( A // C or C // A ) and
A2: ( a <> b & ( a,b // c,d or c,d // a,b ) ) and
A3: ( a in A & b in A ) and
A4: c in C ; :: thesis: d in C
A is being_line by A1, AFF_1:36;
then a,b // A by A3, AFF_1:52;
then c,d // A by A2, Th4;
then c,d // C by A1, Th3;
hence d in C by A4, Th2; :: thesis: verum