set a = the Element of AS;
consider A being Subset of AS such that
the Element of AS in A
and
the Element of AS in A
and
the Element of AS in A
and
A1:
A is being_plane
by AFF_4:37;
A in AfPlanes AS
by A1;
then
Class ((PlanesParallelity AS),A) in Class (PlanesParallelity AS)
by EQREL_1:def 3;
hence
Class (PlanesParallelity AS) is non empty set
; verum