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

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