let A be non empty set ; :: thesis: for a being object of (EnsCat A) holds the_carrier_of a = a
let a be object of (EnsCat A); :: thesis: the_carrier_of a = a
thus the_carrier_of a = proj1 (id a) by Th32
.= dom (id a)
.= a by RELAT_1:45 ; :: thesis: verum