:: deftheorem defines PlanesParallelity AFPROJ:def 4 :
for AS being AffinSpace holds PlanesParallelity AS = { [X,Y] where X, Y is Subset of AS : ( X is being_plane & Y is being_plane & X '||' Y ) } ;