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 A1: ( a,b // M & c,d // M ) by AFF_1:34;
then M is being_line by AFF_1:26;
hence a,b // c,d by A1, AFF_1:31; :: thesis: verum