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 Th31
.= a ; :: thesis: verum