theorem :: AFPROJ:6

for AS being AffinSpace
for A, X, Y being Subset of AS st X is being_plane & A '||' X & X '||' Y holds
A '||' Y by AFF_4:59, AFF_4:60;