let A be non empty AltCatStr ; :: thesis: for B being non empty SubCatStr of A
for o being object of B holds (incl B) . o = o
let B be non empty SubCatStr of A; :: thesis: for o being object of B holds (incl B) . o = o
let o be object of B; :: thesis: (incl B) . o = o
A1: [o,o] in [: the carrier of B, the carrier of B:] by ZFMISC_1:87;
thus (incl B) . o = ((id [: the carrier of B, the carrier of B:]) . [o,o]) `1 by Def29
.= [o,o] `1 by A1, FUNCT_1:18
.= o by MCART_1:7 ; :: thesis: verum