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