theorem Th4: :: CARD_3:4

for x being object
for X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]