:: deftheorem defines Plane AFF_4:def 1 :
for AS being AffinSpace
for K, P being Subset of AS holds Plane (K,P) = { a where a is Element of AS : ex b being Element of AS st
( a,b // K & b in P ) } ;