let E be non empty add-associative addLoopStr ; :: thesis: for A, B, C being Subset of E holds (A + B) + C = A + (B + C)
let A, B, C be Subset of E; :: thesis: (A + B) + C = A + (B + C)
for x being Element of E holds
( x in (A + B) + C iff x in A + (B + C) )
proof
let x be Element of E; :: thesis: ( x in (A + B) + C iff x in A + (B + C) )
hereby :: thesis: ( x in A + (B + C) implies x in (A + B) + C )
assume x in (A + B) + C ; :: thesis: x in A + (B + C)
then consider ab, c being Element of E such that
A1: ( x = ab + c & ab in A + B & c in C ) ;
consider a, b being Element of E such that
A2: ( ab = a + b & a in A & b in B ) by A1;
A3: x = a + (b + c) by ;
b + c in B + C by A1, A2;
hence x in A + (B + C) by A2, A3; :: thesis: verum
end;
assume x in A + (B + C) ; :: thesis: x in (A + B) + C
then consider a, bc being Element of E such that
A4: ( x = a + bc & a in A & bc in B + C ) ;
consider b, c being Element of E such that
A5: ( bc = b + c & b in B & c in C ) by A4;
A6: x = (a + b) + c by ;
a + b in A + B by A4, A5;
hence x in (A + B) + C by A5, A6; :: thesis: verum
end;
hence (A + B) + C = A + (B + C) by SUBSET_1:3; :: thesis: verum