thus
( P c= A implies for a, b being object st [a,b] in P holds
[a,b] in A )
; ( ( for a, b being object st [a,b] in P holds
[a,b] in A ) implies P c= A )
assume A1:
for a, b being object st [a,b] in P holds
[a,b] in A
; P c= A
let x be object ; TARSKI:def 3 ( not x in P or x in A )
assume A2:
x in P
; x in A
then
ex y, z being object st x = [y,z]
by Def1;
hence
x in A
by A1, A2; verum