let BL be Boolean Lattice; :: thesis: for F being Field of BL holds F is ClosedSubset of BL
let F be Field of BL; :: thesis: F is ClosedSubset of BL
A1: for a, b being Element of BL st a in F & b in F holds
a "/\" b in F by Def9;
for a, b being Element of BL st a in F & b in F holds
a "\/" b in F by Th32;
hence F is ClosedSubset of BL by A1, LATTICES:def 24, LATTICES:def 25; :: thesis: verum