set C = the empty CategoryStr opp ;
take the empty CategoryStr opp ; :: thesis: ( the empty CategoryStr opp is strict & the empty CategoryStr opp is empty & the empty CategoryStr opp is discrete & the empty CategoryStr opp is with_identities & the empty CategoryStr opp is composable & the empty CategoryStr opp is associative )
( the empty CategoryStr opp is left_composable & the empty CategoryStr opp is right_composable & the empty CategoryStr opp is with_left_identities & the empty CategoryStr opp is with_right_identities & the empty CategoryStr opp is associative ) by Th4, Th5, Th8;
hence ( the empty CategoryStr opp is strict & the empty CategoryStr opp is empty & the empty CategoryStr opp is discrete & the empty CategoryStr opp is with_identities & the empty CategoryStr opp is composable & the empty CategoryStr opp is associative ) by Lm1; :: thesis: verum