let x, y, z be set ; :: thesis: ( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )
thus [:{x},{y,z}:] = {[x,y],[x,z]} :: thesis: [:{x,y},{z}:] = {[x,z],[y,z]}

proof

now

let v be set ; :: thesis: ( ( v in [:{x},{y,z}:] implies v in {[x,y],[x,z]} ) & ( v in {[x,y],[x,z]} implies v in [:{x},{y,z}:] ) )
thus ( v in [:{x},{y,z}:] implies v in {[x,y],[x,z]} ) :: thesis: ( v in {[x,y],[x,z]} implies v in [:{x},{y,z}:] )

proof

assume v in [:{x},{y,z}:] ; :: thesis: v in {[x,y],[x,z]}
then consider x1, y1 being set such that
A1: ( x1 in {x} & y1 in {y,z} ) and
A2: v = [x1,y1] by Def2;
( x1 = x & ( y1 = y or y1 = z ) ) by A1, TARSKI:def 1, TARSKI:def 2;
hence v in {[x,y],[x,z]} by A2, TARSKI:def 2; :: thesis: verum

end;

assume v in {[x,y],[x,z]} ; :: thesis: v in [:{x},{y,z}:]
then ( ( v = [x,y] or v = [x,z] ) & x in {x} & y in {y,z} & z in {y,z} ) by TARSKI:def 1, TARSKI:def 2;
hence v in [:{x},{y,z}:] by Lm17; :: thesis: verum

end;

hence [:{x},{y,z}:] = {[x,y],[x,z]} by TARSKI:2; :: thesis: verum

end;

now

let v be set ; :: thesis: ( ( v in [:{x,y},{z}:] implies v in {[x,z],[y,z]} ) & ( v in {[x,z],[y,z]} implies v in [:{x,y},{z}:] ) )
thus ( v in [:{x,y},{z}:] implies v in {[x,z],[y,z]} ) :: thesis: ( v in {[x,z],[y,z]} implies v in [:{x,y},{z}:] )

proof

assume v in [:{x,y},{z}:] ; :: thesis: v in {[x,z],[y,z]}
then consider x1, y1 being set such that
A3: ( x1 in {x,y} & y1 in {z} ) and
A4: v = [x1,y1] by Def2;
( y1 = z & ( x1 = x or x1 = y ) ) by A3, TARSKI:def 1, TARSKI:def 2;
hence v in {[x,z],[y,z]} by A4, TARSKI:def 2; :: thesis: verum

end;

assume v in {[x,z],[y,z]} ; :: thesis: v in [:{x,y},{z}:]
then ( ( v = [x,z] or v = [y,z] ) & x in {x,y} & y in {x,y} & z in {z} ) by TARSKI:def 1, TARSKI:def 2;
hence v in [:{x,y},{z}:] by Lm17; :: thesis: verum

end;

hence [:{x,y},{z}:] = {[x,z],[y,z]} by TARSKI:2; :: thesis: verum