let AS be AffinSpace; :: thesis: for a, b, c, d being Element of
for M being Subset of 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 ; :: thesis: for M being Subset of 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 ; :: 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,b // M & c,d // M ) by AFF_1:48;
hence a,b // c,d by AFF_1:40, AFF_1:45; :: thesis: verum