P0: ( A in Class EqBL2Nat & B in Class EqBL2Nat ) ;
consider x being object such that
Q1: ( x in BOOLEAN * & A = Class (EqBL2Nat,x) ) by P0, EQREL_1:def 3;
consider y being object such that
Q2: ( y in BOOLEAN * & B = Class (EqBL2Nat,y) ) by P0, EQREL_1:def 3;
reconsider x = x, y = y as Element of BOOLEAN * by Q1, Q2;
reconsider AB = Class (EqBL2Nat,(x + y)) as Element of Class EqBL2Nat by EQREL_1:def 3;
take AB ; :: thesis: ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB = Class (EqBL2Nat,(x + y)) )
X2: y in B by Q2, EQREL_1:20;
thus ex x, y being Element of BOOLEAN * st
( x in A & y in B & AB = Class (EqBL2Nat,(x + y)) ) by Q1, EQREL_1:20, X2; :: thesis: verum