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:87;
A2: <^o1,o2^> = the Arrows of B . (o1,o2) by ALTCAT_1:def 1
.= the Arrows of B . [o1,o2] ;
A3: (incl B) . o1 = o1 by Th27;
(incl B) . o2 = o2 by Th27;
then A4: <^((incl B) . o1),((incl B) . o2)^> = the Arrows of A . (o1,o2) by A3, ALTCAT_1:def 1
.= 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