theorem Th20: :: AFF_4:20

for AS being AffinSpace
for K, P, Q being Subset of AS st K is being_line & P is being_line & Q is being_line & not K // Q & Q c= Plane (K,P) holds
Plane (K,Q) = Plane (K,P)