theorem Th2: :: MSAFREE1:2

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o, b being object st [o,b] in REL X holds
( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * )