take X = {(1Cat (0,{0}))}; :: thesis: X is categorial
let x be Element of X; :: according to CAT_5:def 5 :: thesis: x is Category
thus x is Category by TARSKI:def 1; :: thesis: verum