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