:: deftheorem Def2 defines |. CLOSURE2:def 2 :
for S being functional set
for b₂ being Function holds
( ( S <> {} implies ( b₂ = |.S.| iff ex A being non empty functional set st
( A = S & dom b₂ = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b₂ holds
b₂ . i = { (x . i) where x is Element of A : verum } ) ) ) ) & ( not S <> {} implies ( b₂ = |.S.| iff b₂ = {} ) ) );