theorem LM700: :: BINARI_6:35

for x being Element of BOOLEAN * holds QuBL2Nat . (Class (EqBL2Nat,x)) = BL2Nat . x