theorem Th15: :: AFPROJ:15

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