thus ex X being set st
for x being object holds
( x in X iff ex y being object st
( y in F₁() & P₁[y,x] ) ) ; :: thesis: verum