theorem :: COMMACAT:3

for y, x being set holds
( the carrier of (1Cat (x,y)) = {x} & the carrier' of (1Cat (x,y)) = {y} ) ;