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