{ F2(s,t) where s, t is Element of F1() : P1[s,t] } c= F1()
proof
let q be
object ;
TARSKI:def 3 ( not q in { F2(s,t) where s, t is Element of F1() : P1[s,t] } or q in F1() )
assume
q in { F2(s,t) where s, t is Element of F1() : P1[s,t] }
;
q in F1()
then
ex
s,
t being
Element of
F1() st
(
q = F2(
s,
t) &
P1[
s,
t] )
;
hence
q in F1()
by A1;
verum
end;
hence
{ F2(s,t) where s, t is Element of F1() : P1[s,t] } is Subset of F1()
; verum