thus ( P c= A implies for a, b being object st [a,b] in P holds
[a,b] in A ) ; :: thesis: ( ( 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 ; :: thesis: P c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in A )
assume A2: x in P ; :: thesis: x in A
then ex y, z being object st x = [y,z] by Def1;
hence x in A by A1, A2; :: thesis: verum