for AS being AffinSpace
for x being set holds
( x in AfPlanes AS iff ex X being Subset of AS st
( x = X & X is being_plane ) ) ;