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
( o in the carrier of D & the carrier of D c= the carrier of C ) by Def11;
hence o is Object of C ; :: thesis: verum