theorem Th8: :: TOPALG_7:8

for T being non empty TopSpace-like unital BinContinuous TopGrStr
for F, G being Function of [:I[01],I[01]:],T
for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)