theorem :: FUNCT_4:4

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