set C = the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr ;
take the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr ; :: thesis: ( the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is strict & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is with_identities & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is composable & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is associative )
thus ( the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is strict & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is with_identities & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is composable & the strict with_left_identities with_right_identities left_composable right_composable associative CategoryStr is associative ) ; :: thesis: verum