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 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