let L be distributive Lattice; :: thesis: F_primeSet L c< PFilters L
A1: F_primeSet L c= PFilters L

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F_primeSet L or x in PFilters L )
assume x in F_primeSet L ; :: thesis: x in PFilters L
then consider F being Filter of L such that
A2: ( x = F & F <> the carrier of L & F is prime ) ;
thus x in PFilters L by A2; :: thesis: verum

end;

not <.L.) in F_primeSet L

proof

assume <.L.) in F_primeSet L ; :: thesis: contradiction
then consider F being Filter of L such that
B1: ( F = <.L.) & F <> the carrier of L & F is prime ) ;
thus contradiction by B1; :: thesis: verum

end;

hence F_primeSet L c< PFilters L by A1; :: thesis: verum