:: deftheorem defines being_plane AFF_4:def 2 :
for AS being AffinSpace
for X being Subset of AS holds
( X is being_plane iff ex K, P being Subset of AS st
( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) );