:: deftheorem Def5 defines dim2 REWRITE3:def 5 :
for x being object
for E being non empty set holds
( ( ex y being object ex u being Element of E ^omega st x = [y,u] implies dim2 (x,E) = x `2 ) & ( ( for y being object
for u being Element of E ^omega holds not x = [y,u] ) implies dim2 (x,E) = {} ) );