let I be set ; :: thesis: for M being ManySortedSet of
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
let M be ManySortedSet of ; :: thesis: for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
let SF be SubsetFamily of M; :: thesis: ( not SF is empty implies for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } )
assume A1: not SF is empty ; :: thesis: for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
then consider A being non empty functional set such that
A2: A = SF and
dom |.SF.| = meet { (dom x) where x is Element of A : verum } and
A3: for i being set st i in dom |.SF.| holds
|.SF.| . i = { (x . i) where x is Element of A : verum } by Def3;
A4: |:SF:| = |.SF.| by A1, Def4;
let i be set ; :: thesis: ( i in I implies |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } )
assume A5: i in I ; :: thesis: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }
A6: dom |:SF:| = I by PARTFUN1:def 4;
set K = { (x . i) where x is Element of Bool M : x in SF } ;
set N = { (x . i) where x is Element of A : verum } ;
{ (x . i) where x is Element of Bool M : x in SF } = { (x . i) where x is Element of A : verum }

proof

thus { (x . i) where x is Element of Bool M : x in SF } c= { (x . i) where x is Element of A : verum } :: according to XBOOLE_0:def 10 :: thesis: { (x . i) where x is Element of A : verum } c= { (x . i) where x is Element of Bool M : x in SF }

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x . i) where x is Element of Bool M : x in SF } or q in { (x . i) where x is Element of A : verum } )
assume q in { (x . i) where x is Element of Bool M : x in SF } ; :: thesis: q in { (x . i) where x is Element of A : verum }
then consider x being Element of Bool M such that
A7: ( q = x . i & x in SF ) ;
thus q in { (x . i) where x is Element of A : verum } by A2, A7; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x . i) where x is Element of A : verum } or q in { (x . i) where x is Element of Bool M : x in SF } )
assume q in { (x . i) where x is Element of A : verum } ; :: thesis: q in { (x . i) where x is Element of Bool M : x in SF }
then consider x being Element of A such that
A8: q = x . i ;
x in SF by A2;
hence q in { (x . i) where x is Element of Bool M : x in SF } by A8; :: thesis: verum

end;

hence |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A3, A4, A5, A6; :: thesis: verum