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 object ; :: 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] and
a in f ;
f is Subset of ([#] L) by WAYBEL_7:2;
hence x in [: the carrier of L,(bool the carrier of L):] by A1, ZFMISC_1:def 2; :: thesis: verum