let C be non empty AltCatStr ; :: thesis: for D being non empty SubCatStr of C
for o being object of D holds o is object of C
let D be non empty SubCatStr of C; :: thesis: for o being object of D holds o is object of C
let o be object of D; :: thesis: o is object of C
A1: o in the carrier of D ;
the carrier of D c= the carrier of C by Def11;
hence o is object of C by A1; :: thesis: verum