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] ) ) from TARSKI_0:sch 1(A1); :: thesis: verum