let A, B be Element of Class EqBL2Nat; A + B = B + A
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;
R0:
( x in A & y in B )
by Q1, Q2, EQREL_1:20;
then R1:
A + B = Class (EqBL2Nat,(x + y))
by LM800;
L1:
B + A = Class (EqBL2Nat,(y + x))
by LM800, R0;
QuBL2Nat . (A + B) =
BL2Nat . (x + y)
by LM700, R1
.=
(BL2Nat . x) + (BL2Nat . y)
by LM240
.=
BL2Nat . (y + x)
by LM240
.=
QuBL2Nat . (B + A)
by L1, LM700
;
hence
A + B = B + A
by FUNCT_2:19; verum