let Y be non empty set ; :: thesis: '/\' ({} ()) = %O Y
for x being set holds
( x in %O Y iff ex h being Function ex F being Subset-Family of Y st
( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} ) )
proof
let x be set ; :: thesis: ( x in %O Y iff ex h being Function ex F being Subset-Family of Y st
( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} ) )

hereby :: thesis: ( ex h being Function ex F being Subset-Family of Y st
( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} ) implies x in %O Y )
reconsider h = {} as Function ;
assume x in %O Y ; :: thesis: ex h being Function ex F being Element of bool (bool Y) st
( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} )

then A1: x in {Y} by PARTIT1:def 8;
take h = h; :: thesis: ex F being Element of bool (bool Y) st
( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} )

take F = {} (bool Y); :: thesis: ( dom h = {} () & rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} )

thus dom h = {} () ; :: thesis: ( rng h = F & ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} )

thus rng h = F ; :: thesis: ( ( for d being set st d in {} () holds
h . d in d ) & x = Intersect F & x <> {} )

thus for d being set st d in {} () holds
h . d in d ; :: thesis: ( x = Intersect F & x <> {} )
x = Y by ;
hence x = Intersect F by SETFAM_1:def 9; :: thesis: x <> {}
thus x <> {} by ; :: thesis: verum
end;
given h being Function, F being Subset-Family of Y such that A2: ( dom h = {} () & rng h = F ) and
for d being set st d in {} () holds
h . d in d and
A3: x = Intersect F and
x <> {} ; :: thesis: x in %O Y
F = {} by ;
then x = Y by ;
then x in {Y} by TARSKI:def 1;
hence x in %O Y by PARTIT1:def 8; :: thesis: verum
end;
hence '/\' ({} ()) = %O Y by BVFUNC_2:def 1; :: thesis: verum