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

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