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