theorem :: AFF_4:15

for AS being AffinSpace
for K, P being Subset of AS st K // P holds
Plane (K,P) = P