AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) is SubCatStr of C
proof
thus
the
carrier of
AltCatStr(# the
carrier of
C,the
Arrows of
C,the
Comp of
C #)
c= the
carrier of
C
;
:: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) cc= the Arrows of C & the Comp of AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) cc= the Comp of C )
thus
the
Arrows of
AltCatStr(# the
carrier of
C,the
Arrows of
C,the
Comp of
C #)
cc= the
Arrows of
C
;
:: thesis: the Comp of AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) cc= the Comp of C
thus
the
Comp of
AltCatStr(# the
carrier of
C,the
Arrows of
C,the
Comp of
C #)
cc= the
Comp of
C
;
:: thesis: verum
end;
then reconsider D = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) as SubCatStr of C ;
reconsider D = D as non empty full id-inheriting SubCatStr of C by Th34, Th35;
take
D
; :: thesis: ( D is full & not D is empty & D is strict )
thus
( D is full & not D is empty & D is strict )
; :: thesis: verum