let C be non empty AltCatStr ; :: thesis: for o being object of C
for o' being object of (ObCat o) holds o' = o
let o be object of C; :: thesis: for o' being object of (ObCat o) holds o' = o
let o' be object of (ObCat o); :: thesis: o' = o
the carrier of (ObCat o) = {o} by Def12;
hence o' = o by TARSKI:def 1; :: thesis: verum