let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₁[s,t] } or x in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₂[s1,t1] } )
assume x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₁[s,t] } ; :: thesis: x in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₂[s1,t1] }
then consider s being Element of F₁(), t being Element of F₂() such that
A2: x = F₃(s,t) and
A3: P₁[s,t] ;
ex s9 being Element of F₁() st
( P₂[s9,t] & F₃(s,t) = F₃(s9,t) ) by A1, A3;
hence x in { F₃(s1,t1) where s1 is Element of F₁(), t1 is Element of F₂() : P₂[s1,t1] } by A2; :: thesis: verum