for x being Element of BOOLEAN * holds BL2Nat . x = ExAbsval x by Def110;
hence BL2Nat is onto by LM220; :: thesis: verum