theorem Th5: :: FUNCT_4:5

for X, Y being set
for a, b being object st X --> a c= Y --> b holds
X c= Y