let A be non empty AltCatStr ; 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; for o1, o2 being Object of B holds <^o1,o2^> c= <^((incl B) . o1),((incl B) . o2)^>
let o1, o2 be Object of B; <^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; verum