take <*> the non empty set ; :: thesis: <*> the non empty set is B,R -correct
thus <*> the non empty set is B,R -correct ; :: thesis: verum