let AS be AffinSpace; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane holds
( PDir X = PDir Y iff X '||' Y )
let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane implies ( PDir X = PDir Y iff X '||' Y ) )
assume A1: ( X is being_plane & Y is being_plane ) ; :: thesis: ( PDir X = PDir Y iff X '||' Y )
then A2: ( Y in AfPlanes AS & X in AfPlanes AS ) ;
A3: ( PDir X = Class (PlanesParallelity AS),X & PDir Y = Class (PlanesParallelity AS),Y ) by A1, Def6;

A4: now

assume PDir X = PDir Y ; :: thesis: X '||' Y
then X in Class (PlanesParallelity AS),Y by A2, A3, EQREL_1:31;
then ex Y' being Subset of AS st
( X = Y' & Y' is being_plane & Y '||' Y' ) by A1, A3, Th10;
hence X '||' Y by A1, AFF_4:58; :: thesis: verum

end;

now

assume X '||' Y ; :: thesis: PDir X = PDir Y
then Y in Class (PlanesParallelity AS),X by A1, A3, Th10;
hence PDir X = PDir Y by A2, A3, EQREL_1:31; :: thesis: verum

end;

hence ( PDir X = PDir Y iff X '||' Y ) by A4; :: thesis: verum