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