reconsider C = CatStr(# {0 },{1},(1 :-> 0 ),(1 :-> 0 ),(1,1 :-> 1),(0 :-> 1) #) as non empty non void CatStr ;
take C ; :: thesis: ( C is Category-like & not C is void & not C is empty & C is strict )
thus ( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . (the Comp of C . g,f) = the Source of C . f & the Target of C . (the Comp of C . g,f) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . h,(the Comp of C . g,f) = the Comp of C . (the Comp of C . h,g),f ) & ( for b being Element of the carrier of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C st the Source of C . g = b holds
the Comp of C . g,(the Id of C . b) = g ) ) ) ) by Lm1; :: according to CAT_1:def 8 :: thesis: ( not C is void & not C is empty & C is strict )
thus ( not C is void & not C is empty & C is strict ) ; :: thesis: verum