consider a, b, c being Element of AS;
consider A being Subset of AS such that
a in A
and
b in A
and
c 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 5;
hence
Class (PlanesParallelity AS) is non empty set
; verum