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

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