let AS be AffinSpace; 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; 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; ( ( 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
; ( a,b // K & b,a // K )
a,b // A
by A1, AFF_1:34;
hence
a,b // K
by A2, AFF_1:43; b,a // K
hence
b,a // K
by AFF_1:34; verum