set D = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #);
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 & 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 ) ; :: according to ALTCAT_2:def 11 :: thesis: verum

end;

then reconsider D = AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) as SubCatStr of C ;
take D ; :: thesis: ( D is full & not D is empty & D is strict )
dom the Arrows of C = [:the carrier of D,the carrier of D:] by PARTFUN1:def 4;
hence the Arrows of D = the Arrows of C || the carrier of D by RELAT_1:98; :: according to ALTCAT_2:def 13 :: thesis: ( not D is empty & D is strict )
thus not the carrier of D is empty ; :: according to STRUCT_0:def 1 :: thesis: D is strict
thus D is strict ; :: thesis: verum