theorem LM800: :: BINARI_6:36

for A, B being Element of Class EqBL2Nat
for x, y being Element of BOOLEAN * st x in A & y in B holds
A + B = Class (EqBL2Nat,(x + y))