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