set Q1 = { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } ;
{ g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } c= HFuncs NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } or x in HFuncs NAT )
assume x in { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } ; :: thesis: x in HFuncs NAT
then ex g being Element of HFuncs NAT st
( x = g & ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) ) ;
hence x in HFuncs NAT ; :: thesis: verum

end;

hence Q \/ { g where g is Element of HFuncs NAT : ex f1, f2 being Element of HFuncs NAT ex i being Element of NAT st
( f1 in Q & f2 in Q & g is_primitive-recursively_expressed_by f1,f2,i ) } is Subset of (HFuncs NAT) by XBOOLE_1:8; :: thesis: verum