let x, y be object ; :: thesis: [:{x},{y}:] = {[x,y]}

now :: thesis: for z being object holds
( ( z in [:{x},{y}:] implies z in {[x,y]} ) & ( z in {[x,y]} implies z in [:{x},{y}:] ) )

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

proof

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

end;

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

end;

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