let x, y, z be object ; :: thesis: ( [:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]} )
now :: thesis: for v being object holds
( ( v in [:{x},{y,z}:] implies v in {[x,y],[x,z]} ) & ( v in {[x,y],[x,z]} implies v in [:{x},{y,z}:] ) )
let v be object ; :: 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}:] ) )
A1: z in {y,z} by TARSKI:def 2;
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 object such that
A2: x1 in {x} and
A3: y1 in {y,z} and
A4: v = [x1,y1] by Def2;
A5: ( y1 = y or y1 = z ) by A3, TARSKI:def 2;
x1 = x by A2, TARSKI:def 1;
hence v in {[x,y],[x,z]} by A4, A5, TARSKI:def 2; :: thesis: verum
end;
assume v in {[x,y],[x,z]} ; :: thesis: v in [:{x},{y,z}:]
then A6: ( v = [x,y] or v = [x,z] ) by TARSKI:def 2;
( x in {x} & y in {y,z} ) by TARSKI:def 1, TARSKI:def 2;
hence v in [:{x},{y,z}:] by A6, A1, Lm16; :: thesis: verum
end;
hence [:{x},{y,z}:] = {[x,y],[x,z]} by TARSKI:2; :: thesis: [:{x,y},{z}:] = {[x,z],[y,z]}
now :: thesis: for v being object holds
( ( v in [:{x,y},{z}:] implies v in {[x,z],[y,z]} ) & ( v in {[x,z],[y,z]} implies v in [:{x,y},{z}:] ) )
let v be object ; :: 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}:] ) )
A7: z in {z} by TARSKI:def 1;
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 object such that
A8: x1 in {x,y} and
A9: y1 in {z} and
A10: v = [x1,y1] by Def2;
A11: ( x1 = x or x1 = y ) by A8, TARSKI:def 2;
y1 = z by A9, TARSKI:def 1;
hence v in {[x,z],[y,z]} by A10, A11, TARSKI:def 2; :: thesis: verum
end;
assume v in {[x,z],[y,z]} ; :: thesis: v in [:{x,y},{z}:]
then A12: ( v = [x,z] or v = [y,z] ) by TARSKI:def 2;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence v in [:{x,y},{z}:] by A12, A7, Lm16; :: thesis: verum
end;
hence [:{x,y},{z}:] = {[x,z],[y,z]} by TARSKI:2; :: thesis: verum