let UN be Universe; :: thesis: for u, v being Element of UN holds {[u,{}],[v,{{}}]} = [:{u},{{}}:] \/ [:{v},{{{}}}:]
let u, v be Element of UN; :: thesis: {[u,{}],[v,{{}}]} = [:{u},{{}}:] \/ [:{v},{{{}}}:]
set S1 = {[u,{}],[v,{{}}]};
set S2 = [:{u},{{}}:] \/ [:{v},{{{}}}:];

now :: thesis: ( {[u,{}],[v,{{}}]} c= [:{u},{{}}:] \/ [:{v},{{{}}}:] & [:{u},{{}}:] \/ [:{v},{{{}}}:] c= {[u,{}],[v,{{}}]} )

now :: thesis: for o being object st o in {[u,{}],[v,{{}}]} holds
o in [:{u},{{}}:] \/ [:{v},{{{}}}:]

let o be object ; :: thesis: ( o in {[u,{}],[v,{{}}]} implies o in [:{u},{{}}:] \/ [:{v},{{{}}}:] )
assume o in {[u,{}],[v,{{}}]} ; :: thesis: o in [:{u},{{}}:] \/ [:{v},{{{}}}:]
then ( o = [u,{}] or o = [v,{{}}] ) by TARSKI:def 2;
then ( o in [:{u},{{}}:] or o in [:{v},{{{}}}:] ) by ZFMISC_1:28;
hence o in [:{u},{{}}:] \/ [:{v},{{{}}}:] by XBOOLE_0:def 3; :: thesis: verum

end;

hence {[u,{}],[v,{{}}]} c= [:{u},{{}}:] \/ [:{v},{{{}}}:] ; :: thesis: [:{u},{{}}:] \/ [:{v},{{{}}}:] c= {[u,{}],[v,{{}}]}

now :: thesis: for o being object st o in [:{u},{{}}:] \/ [:{v},{{{}}}:] holds
o in {[u,{}],[v,{{}}]}

let o be object ; :: thesis: ( o in [:{u},{{}}:] \/ [:{v},{{{}}}:] implies o in {[u,{}],[v,{{}}]} )
assume o in [:{u},{{}}:] \/ [:{v},{{{}}}:] ; :: thesis: o in {[u,{}],[v,{{}}]}
then ( o in [:{u},{{}}:] or o in [:{v},{{{}}}:] ) by XBOOLE_0:def 3;
then ( o in {[u,{}]} or o in {[v,{{}}]} ) by ZFMISC_1:29;
then ( o = [u,{}] or o = [v,{{}}] ) by TARSKI:def 1;
hence o in {[u,{}],[v,{{}}]} by TARSKI:def 2; :: thesis: verum

end;

hence [:{u},{{}}:] \/ [:{v},{{{}}}:] c= {[u,{}],[v,{{}}]} ; :: thesis: verum

end;

hence {[u,{}],[v,{{}}]} = [:{u},{{}}:] \/ [:{v},{{{}}}:] ; :: thesis: verum