theorem Th19: :: AFPROJ:19

for AS being AffinSpace
for x being set holds
( x in [:(Dir_of_Planes AS),{2}:] iff ex X being Subset of AS st
( x = [(PDir X),2] & X is being_plane ) )