let a, b, c, d be object ; :: thesis: {a,d} \/ {b,c} = {a,b,c,d}
set x1 = a;
set x2 = d;
set x3 = b;
set x4 = c;
{a,d} \/ {b,c} = {a,d,b,c} by ENUMSET1:5
.= {a,b,c,d} by ENUMSET1:63 ;
hence {a,d} \/ {b,c} = {a,b,c,d} ; :: thesis: verum