theorem Th5: :: CLASSES5:5

for X, Y being non empty set
for y being Element of Y holds [:X,{y}:] c= union (Funcs (X,Y))