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