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
for a, b being Element of BL st a in F & b in F holds
( a "/\" b in F & a "\/" b in F ) by Def14, Th39;
hence F is ClosedSubset of BL by Def10; :: thesis: verum