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