let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for M being Subset of AS st ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) holds
a,b // c,d
let a, b, c, d be Element of AS; :: thesis: for M being Subset of AS st ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) holds
a,b // c,d
let M be Subset of AS; :: thesis: ( ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) implies a,b // c,d )
assume ( ( a,b // M or b,a // M ) & ( c,d // M or d,c // M ) ) ; :: thesis: a,b // c,d
then A: ( a,b // M & c,d // M ) by AFF_1:48;
then M is being_line by AFF_1:40;
hence a,b // c,d by A, AFF_1:45; :: thesis: verum