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 Def28
.= [o,o] `1 by A1, FUNCT_1:18
.= o ; :: thesis: verum