x `2 = x `2 ;
hence x `2 is Element of Y2 ; :: thesis: verum