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 ( a in F & b in F ) ; :: thesis: a "\/" b in F
then ( a ` in F & b ` in F ) by Def9;
then (a `) "/\" (b `) in F by Def9;
then (a "\/" b) ` in F by LATTICES:24;
then ((a "\/" b) `) ` in F by Def9;
hence a "\/" b in F ; :: thesis: verum