let AS be AffinSpace; :: thesis: 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 ) )
let x be set ; :: thesis: ( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) )

A1: now :: thesis: ( x in Dir_of_Planes AS implies ex X being Subset of AS st
( x = PDir X & X is being_plane ) )

assume A2: x in Dir_of_Planes AS ; :: thesis: ex X being Subset of AS st
( x = PDir X & X is being_plane )
then reconsider x99 = x as Subset of (AfPlanes AS) ;
consider x9 being object such that
A3: x9 in AfPlanes AS and
A4: x99 = Class ((PlanesParallelity AS),x9) by A2, EQREL_1:def 3;
consider X being Subset of AS such that
A5: x9 = X and
A6: X is being_plane by A3;
take X = X; :: thesis: ( x = PDir X & X is being_plane )
thus x = PDir X by A4, A5; :: thesis: X is being_plane
thus X is being_plane by A6; :: thesis: verum

end;

now :: thesis: ( ex X being Subset of AS st
( x = PDir X & X is being_plane ) implies x in Dir_of_Planes AS )

given X being Subset of AS such that A7: x = PDir X and
A8: X is being_plane ; :: thesis: x in Dir_of_Planes AS
X in AfPlanes AS by A8;
hence x in Dir_of_Planes AS by A7, EQREL_1:def 3; :: thesis: verum

end;

hence ( x in Dir_of_Planes AS iff ex X being Subset of AS st
( x = PDir X & X is being_plane ) ) by A1; :: thesis: verum