theorem Th3: :: AFPROJ:3
for AS being AffinSpace
for X, Y being Subset of AS st AS is AffinPlane & X is being_plane & Y is being_plane holds
X = Y