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

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