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