let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_plane holds
for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let X be Subset of AS; :: thesis: ( X is being_plane implies for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) )
assume A1: X is being_plane ; :: thesis: for x being set holds
( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )
let x be set ; :: thesis: ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) )

A2: now

assume x in PDir X ; :: thesis: ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y )
then x in Class (PlanesParallelity AS),X by A1, Def6;
then [x,X] in PlanesParallelity AS by EQREL_1:27;
then consider K, M being Subset of AS such that
A3: [x,X] = [K,M] and
A4: ( K is being_plane & M is being_plane & K '||' M ) ;
A5: ( x = K & X = M ) by A3, ZFMISC_1:33;
take Y = K; :: thesis: ( x = Y & Y is being_plane & X '||' Y )
thus ( x = Y & Y is being_plane & X '||' Y ) by A4, A5, AFF_4:58; :: thesis: verum

end;

now

given Y being Subset of AS such that A6: ( x = Y & Y is being_plane & X '||' Y ) ; :: thesis: x in PDir X
Y '||' X by A1, A6, AFF_4:58;
then [Y,X] in { [K,M] where K, M is Subset of AS : ( K is being_plane & M is being_plane & K '||' M ) } by A1, A6;
then Y in Class (PlanesParallelity AS),X by EQREL_1:27;
hence x in PDir X by A1, A6, Def6; :: thesis: verum

end;

hence ( x in PDir X iff ex Y being Subset of AS st
( x = Y & Y is being_plane & X '||' Y ) ) by A2; :: thesis: verum