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

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