let R1, R2 be RelStr ; :: thesis: ( union_of R1,R2 = union_of R2,R1 & sum_of R1,R2 = sum_of R2,R1 )
set U1 = union_of R1,R2;
set S1 = sum_of R1,R2;
A1: the carrier of (union_of R1,R2) = the carrier of R2 \/ the carrier of R1 by NECKLA_2:def 2;
A2: the InternalRel of (union_of R1,R2) = the InternalRel of R2 \/ the InternalRel of R1 by NECKLA_2:def 2;
A3: the carrier of (sum_of R1,R2) = the carrier of R2 \/ the carrier of R1 by NECKLA_2:def 3;
the InternalRel of (sum_of R1,R2) = ((the InternalRel of R1 \/ the InternalRel of R2) \/ [:the carrier of R1,the carrier of R2:]) \/ [:the carrier of R2,the carrier of R1:] by NECKLA_2:def 3
.= ((the InternalRel of R2 \/ the InternalRel of R1) \/ [:the carrier of R2,the carrier of R1:]) \/ [:the carrier of R1,the carrier of R2:] by XBOOLE_1:4 ;
hence ( union_of R1,R2 = union_of R2,R1 & sum_of R1,R2 = sum_of R2,R1 ) by A1, A2, A3, NECKLA_2:def 2, NECKLA_2:def 3; :: thesis: verum