take <*> the carrier of R ; :: thesis: <*> the carrier of R is trivial
thus <*> the carrier of R is trivial by ll; :: thesis: verum