reconsider f = PrimeFilters L as Function ;
A1: dom f = the carrier of L by Def6;
rng f c= bool (PFilters L)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (PFilters L) )
reconsider yy = y as set by TARSKI:1;
assume y in rng f ; :: thesis: y in bool (PFilters L)
then consider x being object such that
A2: x in dom f and
A3: y = f . x by FUNCT_1:def 3;
y = { F where F is Filter of L : ( F is prime & x in F ) } by A1, A2, A3, Def6;
then yy c= PFilters L by A1, A2, Th16;
hence y in bool (PFilters L) ; :: thesis: verum

end;

then reconsider f = f as Function of the carrier of L,(bool (PFilters L)) by A1, FUNCT_2:def 1, RELSET_1:4;
for a being Element of L holds f . a = { F where F is Filter of L : ( F is prime & a in F ) } by Def6;
hence PrimeFilters L is Function of the carrier of L,(bool (PFilters L)) ; :: thesis: verum