let L be Lattice; :: thesis: for A being Subset of L holds
( not L = BooleLatt {{}} or A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}} )
let A be Subset of L; :: thesis: ( not L = BooleLatt {{}} or A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}} )
assume L = BooleLatt {{}} ; :: thesis: ( A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}} )
then A2: the carrier of L = bool {{}} by LATTICE3:def 1;
bool {{}} = {{},{{}}} by ZFMISC_1:24;
hence ( A = {} or A = {{}} or A = {{},{{}}} or A = {{{}}} ) by ZFMISC_1:36, A2; :: thesis: verum