set C1 = the with_left_identities non with_right_identities associative composable CategoryStr ;
set C = the with_left_identities non with_right_identities associative composable CategoryStr opp ;
take the with_left_identities non with_right_identities associative composable CategoryStr opp ; :: thesis: ( not the with_left_identities non with_right_identities associative composable CategoryStr opp is with_left_identities & the with_left_identities non with_right_identities associative composable CategoryStr opp is with_right_identities & the with_left_identities non with_right_identities associative composable CategoryStr opp is composable & the with_left_identities non with_right_identities associative composable CategoryStr opp is associative )
thus not the with_left_identities non with_right_identities associative composable CategoryStr opp is with_left_identities by Th7; :: thesis: ( the with_left_identities non with_right_identities associative composable CategoryStr opp is with_right_identities & the with_left_identities non with_right_identities associative composable CategoryStr opp is composable & the with_left_identities non with_right_identities associative composable CategoryStr opp is associative )
thus the with_left_identities non with_right_identities associative composable CategoryStr opp is with_right_identities by Th6; :: thesis: ( the with_left_identities non with_right_identities associative composable CategoryStr opp is composable & the with_left_identities non with_right_identities associative composable CategoryStr opp is associative )
thus the with_left_identities non with_right_identities associative composable CategoryStr opp is composable by Th4, Th5, Def11; :: thesis: the with_left_identities non with_right_identities associative composable CategoryStr opp is associative
thus the with_left_identities non with_right_identities associative composable CategoryStr opp is associative by Th8; :: thesis: verum