:: deftheorem Def15 defines LenMax BINARI_6:def 3 :
for x, y being Element of BOOLEAN * st len x <> 0 & len y <> 0 holds
LenMax (x,y) = max ((len x),(len y));