let L be LATTICE; :: thesis: for F being non empty Subset of (BoolePoset ([#] L)) holds { [a,f] where a is Element of L, f is Element of F : a in f } c= [:the carrier of L,(bool the carrier of L):]
let F be non empty Subset of (BoolePoset ([#] L)); :: thesis: { [a,f] where a is Element of L, f is Element of F : a in f } c= [:the carrier of L,(bool the carrier of L):]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [a,f] where a is Element of L, f is Element of F : a in f } or x in [:the carrier of L,(bool the carrier of L):] )
assume x in { [a,f] where a is Element of L, f is Element of F : a in f } ; :: thesis: x in [:the carrier of L,(bool the carrier of L):]
then consider a being Element of L, f being Element of F such that
A1: ( x = [a,f] & a in f ) ;
f is Subset of ([#] L) by WAYBEL_7:4;
hence x in [:the carrier of L,(bool the carrier of L):] by A1, ZFMISC_1:def 2; :: thesis: verum