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