thus ( ex y being object ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) ; :: thesis: ( ( for y being object
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega )
{} = <%> E ;
hence ( ( for y being object
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) ; :: thesis: verum