let Y be non empty set ; :: thesis: '/\' ({} (PARTITIONS Y)) = %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 = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) 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 = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) 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 = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) 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 = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) 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 = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
take F = {} (bool Y); :: thesis: ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus dom h = {} (PARTITIONS Y) ; :: thesis: ( rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus rng h = F ; :: thesis: ( ( for d being set st d in {} (PARTITIONS Y) holds
h . d in d ) & x = Intersect F & x <> {} )
thus for d being set st d in {} (PARTITIONS Y) holds
h . d in d ; :: thesis: ( x = Intersect F & x <> {} )
x = Y by A1, TARSKI:def 1;
hence x = Intersect F by SETFAM_1:def 9; :: thesis: x <> {}
thus x <> {} by A1, TARSKI:def 1; :: thesis: verum

end;

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

end;

hence '/\' ({} (PARTITIONS Y)) = %O Y by BVFUNC_2:def 1; :: thesis: verum