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