theorem Th58: :: AFF_4:58

for AS being AffinSpace
for X, Y being Subset of AS st X is being_plane & Y is being_plane & X '||' Y holds
Y '||' X