let AS be AffinSpace; :: thesis: for a, b, c, d being Element of AS
for A being Subset of AS st ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) & a <> b holds
( c,d // A & d,c // A )
let a, b, c, d be Element of AS; :: thesis: for A being Subset of AS st ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) & a <> b holds
( c,d // A & d,c // A )
let A be Subset of AS; :: thesis: ( ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) & a <> b implies ( c,d // A & d,c // A ) )
assume that
A1: ( ( a,b // A or b,a // A ) & ( a,b // c,d or c,d // a,b ) ) and
A2: a <> b ; :: thesis: ( c,d // A & d,c // A )
( a,b // A & a,b // c,d ) by A1, AFF_1:4, AFF_1:34;
hence c,d // A by A2, AFF_1:32; :: thesis: d,c // A
hence d,c // A by AFF_1:34; :: thesis: verum