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

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