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 and
A3: ( y in Z & z = [x,y] ) by Def2;
x in Y by A1, A2, TARSKI:def 3;
hence z in [:Y,Z:] by 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 and
A5: x in X and
A6: z = [y,x] by Def2;
x in Y by A1, A5, TARSKI:def 3;
hence z in [:Z,Y:] by A4, A6, Def2; :: thesis: verum