scheme :: DOMAIN_1:sch 6
Fraenkel6{ P₁[ object ], P₂[ object ] } :

for X1 being non empty set st ( for x1 being Element of X1 holds
( P₁[x1] iff P₂[x1] ) ) holds
{ y1 where y1 is Element of X1 : P₁[y1] } = { z1 where z1 is Element of X1 : P₂[z1] }