let A, B, C be Element of Class EqBL2Nat; (A + B) + C = A + (B + C)
P0:
( A in Class EqBL2Nat & B in Class EqBL2Nat & C 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;
consider z being object such that
Q3:
( z in BOOLEAN * & C = Class (EqBL2Nat,z) )
by P0, EQREL_1:def 3;
reconsider x = x, y = y, z = z as Element of BOOLEAN * by Q1, Q2, Q3;
R0:
( x in A & y in B & z in C )
by Q1, Q2, Q3, EQREL_1:20;
then R1:
A + B = Class (EqBL2Nat,(x + y))
by LM800;
x + y in A + B
by R1, EQREL_1:20;
then R2:
(A + B) + C = Class (EqBL2Nat,((x + y) + z))
by LM800, R0;
L1:
B + C = Class (EqBL2Nat,(y + z))
by LM800, R0;
y + z in B + C
by L1, EQREL_1:20;
then L2:
A + (B + C) = Class (EqBL2Nat,(x + (y + z)))
by LM800, R0;
QuBL2Nat . ((A + B) + C) =
BL2Nat . ((x + y) + z)
by LM700, R2
.=
(BL2Nat . (x + y)) + (BL2Nat . z)
by LM240
.=
((BL2Nat . x) + (BL2Nat . y)) + (BL2Nat . z)
by LM240
.=
(BL2Nat . x) + ((BL2Nat . y) + (BL2Nat . z))
.=
(BL2Nat . x) + (BL2Nat . (y + z))
by LM240
.=
BL2Nat . (x + (y + z))
by LM240
.=
QuBL2Nat . (A + (B + C))
by L2, LM700
;
hence
(A + B) + C = A + (B + C)
by FUNCT_2:19; verum