theorem Th11: :: JORDAN1H:11
for f being FinSequence of (TOP-REAL 2) holds Y_axis f = proj2 * f