theorem LM930: :: BINARI_6:40

for n being Nat
for z, z1 being Element of BOOLEAN * st z = <*> BOOLEAN & z1 = 0* n holds
Class (EqBL2Nat,z) = Class (EqBL2Nat,z1)