let BL be Boolean Lattice; :: thesis: the carrier of BL is Field of BL

the carrier of BL c= the carrier of BL ;

then reconsider F = the carrier of BL as non empty Subset of BL ;

for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F ) ;

hence the carrier of BL is Field of BL by Def9; :: thesis: verum

the carrier of BL c= the carrier of BL ;

then reconsider F = the carrier of BL as non empty Subset of BL ;

for a, b being Element of BL st a in F & b in F holds

( a "/\" b in F & a ` in F ) ;

hence the carrier of BL is Field of BL by Def9; :: thesis: verum