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