let BL be Boolean Lattice; :: thesis: for a, b being Element of BL
for F being Field of BL st a in F & b in F holds
a => b in F
let a, b be Element of BL; :: thesis: for F being Field of BL st a in F & b in F holds
a => b in F
let F be Field of BL; :: thesis: ( a in F & b in F implies a => b in F )
assume that
A1: a in F and
A2: b in F ; :: thesis: a => b in F
a ` in F by A1, Def9;
then (a `) "\/" b in F by A2, Th32;
hence a => b in F by FILTER_0:42; :: thesis: verum