let o, m be set ; :: thesis: for a, b being Object of (c1Cat* o,m) holds a = b
let a, b be Object of (c1Cat* o,m); :: thesis: a = b
( a = o & b = o ) by TARSKI:def 1;
hence a = b ; :: thesis: verum