let I be set ; :: thesis: for M being ManySortedSet of I
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 I; :: 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 } )
A1: dom |:SF:| = I by PARTFUN1:def 2;
assume A2: 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
A3: A = SF and
dom |.SF.| = meet { (dom x) where x is Element of A : verum } and
A4: for i being set st i in dom |.SF.| holds
|.SF.| . i = { (x . i) where x is Element of A : verum } by Def2;
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 }
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 } ;
A6: { (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 object ; :: 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 ex x being Element of Bool M st
( q = x . i & x in SF ) ;
hence q in { (x . i) where x is Element of A : verum } by A3; :: thesis: verum

end;

let q be object ; :: 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
A7: q = x . i ;
x in SF by A3;
hence q in { (x . i) where x is Element of Bool M : x in SF } by A7; :: thesis: verum

end;

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