let UN be Universe; :: thesis: for u, v being Element of UN holds { f where f is Function of u,v : verum } is Element of UN
let u, v be Element of UN; :: thesis: { f where f is Function of u,v : verum } is Element of UN
set S = { f where f is Function of u,v : verum } ;
{ f where f is Function of u,v : verum } is Subset of (bool [:u,v:])

proof

now :: thesis: for o being object st o in { f where f is Function of u,v : verum } holds
o in bool [:u,v:]

let o be object ; :: thesis: ( o in { f where f is Function of u,v : verum } implies o in bool [:u,v:] )
assume o in { f where f is Function of u,v : verum } ; :: thesis: o in bool [:u,v:]
then ex f being Function of u,v st o = f ;
hence o in bool [:u,v:] ; :: thesis: verum

end;

then { f where f is Function of u,v : verum } c= bool [:u,v:] ;
hence { f where f is Function of u,v : verum } is Subset of (bool [:u,v:]) ; :: thesis: verum

end;

hence { f where f is Function of u,v : verum } is Element of UN by Th13; :: thesis: verum