take 1Cat (0,0) ; :: thesis: ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict )
thus ( 1Cat (0,0) is reflexive & 1Cat (0,0) is transitive & 1Cat (0,0) is associative & 1Cat (0,0) is with_identities & 1Cat (0,0) is Category-like & not 1Cat (0,0) is void & not 1Cat (0,0) is empty & 1Cat (0,0) is strict ) ; :: thesis: verum