let X, Y, Z be set ; :: thesis: ( X c= Y implies ( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] ) )
assume A1: X c= Y ; :: thesis: ( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )
thus [:X,Z:] c= [:Y,Z:] :: thesis: [:Z,X:] c= [:Z,Y:]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X,Z:] or z in [:Y,Z:] )
assume z in [:X,Z:] ; :: thesis: z in [:Y,Z:]
then consider x, y being set such that
A2: ( x in X & y in Z ) and
A3: z = [x,y] by Def2;
x in Y by A1, A2, TARSKI:def 3;
hence z in [:Y,Z:] by A2, A3, Def2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:Z,X:] or z in [:Z,Y:] )
assume z in [:Z,X:] ; :: thesis: z in [:Z,Y:]
then consider y, x being set such that
A4: ( y in Z & x in X ) and
A5: z = [y,x] by Def2;
x in Y by A1, A4, TARSKI:def 3;
hence z in [:Z,Y:] by A4, A5, Def2; :: thesis: verum