:: deftheorem Def3 defines * AFF_4:def 3 :
for AS being AffinSpace
for a being Element of AS
for K being Subset of AS st K is being_line holds
for b₄ being Subset of AS holds
( b₄ = a * K iff ( a in b₄ & K // b₄ ) );