let L be upper-bounded LATTICE; :: thesis: for f being Function of L,(BoolePoset {{}})
for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
let f be Function of L,(BoolePoset {{}}); :: thesis: for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
let p be prime Element of L; :: thesis: ( chi (((downarrow p) `), the carrier of L) = f implies ( f is meet-preserving & f is join-preserving ) )
assume chi (((downarrow p) `), the carrier of L) = f ; :: thesis: ( f is meet-preserving & f is join-preserving )
then for x being Element of L holds
( f . x = {} iff x <= p ) by Th32;
hence ( f is meet-preserving & f is join-preserving ) by Th25; :: thesis: verum