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 (sum_of (R1,R2)) = the carrier of R2 \/ the carrier of R1 by NECKLA_2:def 3;
A2: 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 ;
( the carrier of (union_of (R1,R2)) = the carrier of R2 \/ the carrier of R1 & the InternalRel of (union_of (R1,R2)) = the InternalRel of R2 \/ the InternalRel of R1 ) by NECKLA_2:def 2;
hence ( union_of (R1,R2) = union_of (R2,R1) & sum_of (R1,R2) = sum_of (R2,R1) ) by A1, A2, NECKLA_2:def 2, NECKLA_2:def 3; :: thesis: verum