let A be non empty AltCatStr ; :: thesis: for B being non empty SubCatStr of A
for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
let B be non empty SubCatStr of A; :: thesis: for o1, o2 being object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
let o1, o2 be object of B; :: thesis: <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
A1: [o1,o2] in [: the carrier of B, the carrier of B:] by ZFMISC_1:106;
A2: <^o1,o2^> = the Arrows of B . (o1,o2) by ALTCAT_1:def 2
.= the Arrows of B . [o1,o2] ;
A3: (incl B) . o1 = o1 by Th28;
(incl B) . o2 = o2 by Th28;
then A4: <^((incl B) . o1),((incl B) . o2)^> = the Arrows of A . (o1,o2) by A3, ALTCAT_1:def 2
.= the Arrows of A . [o1,o2] ;
the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;
hence <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^> by A1, A2, A4, ALTCAT_2:def 2; :: thesis: verum