let x be Element of BOOLEAN * ; :: thesis: QuBL2Nat . (Class (EqBL2Nat,x)) = BL2Nat . x
reconsider A = Class (EqBL2Nat,x) as Element of Class EqBL2Nat by EQREL_1:def 3;
reconsider A0 = A as Subset of (BOOLEAN *) ;
consider x1 being object such that
P1: ( x1 in A0 & QuBL2Nat . A0 = BL2Nat . x1 ) by Def400;
reconsider x1 = x1 as Element of BOOLEAN * by P1;
Class (EqBL2Nat,x1) = Class (EqBL2Nat,x) by P1, EQREL_1:23;
then [x1,x] in EqBL2Nat by EQREL_1:35;
hence QuBL2Nat . (Class (EqBL2Nat,x)) = BL2Nat . x by P1, Def300; :: thesis: verum