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 that
A1: X is being_plane and
A2: Y is being_plane ; :: thesis: ( PDir X = PDir Y iff X '||' Y )
A3: PDir Y = Class ((PlanesParallelity AS),Y) ;
A4: Y in AfPlanes AS by A2;
A5: now :: thesis: ( PDir X = PDir Y implies X '||' Y )
assume PDir X = PDir Y ; :: thesis: X '||' Y
then X in Class ((PlanesParallelity AS),Y) by A4, EQREL_1:23;
then ex Y9 being Subset of AS st
( X = Y9 & Y9 is being_plane & Y '||' Y9 ) by A2, A3, Th10;
hence X '||' Y by A2, AFF_4:58; :: thesis: verum
end;
A6: PDir X = Class ((PlanesParallelity AS),X) ;
A7: X in AfPlanes AS by A1;
now :: thesis: ( X '||' Y implies PDir X = PDir Y )
assume X '||' Y ; :: thesis: PDir X = PDir Y
then Y in Class ((PlanesParallelity AS),X) by A1, A2, A6, Th10;
hence PDir X = PDir Y by A7, EQREL_1:23; :: thesis: verum
end;
hence ( PDir X = PDir Y iff X '||' Y ) by A5; :: thesis: verum