theorem Th5: :: JORDAN12:5

for g1, g2 being FinSequence of (TOP-REAL 2) holds L~ g1 c= L~ (g1 ^' g2)