thus Class R,x is Element of Class R by Def5; :: thesis: verum