:: deftheorem defines '||' AFF_4:def 4 :
for AS being AffinSpace
for X, Y being Subset of AS holds
( X '||' Y iff for a being Element of AS
for A being Subset of AS st a in Y & A is being_line & A c= X holds
a * A c= Y );