x `1 = x `1 ;
hence x `1 is Element of Y1 ; :: thesis: verum