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