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