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