let Y be non empty set ; :: thesis:
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 <> {} ) )

let x be set ; :: thesis:

hereby :: thesis:

reconsider h = {} as Function ;
assume x in %O Y ; :: thesis:
then A1: x in {Y} by PARTIT1:def 8;
take h = h; :: thesis:
take F = {} (bool Y); :: thesis:
thus dom h = {} (PARTITIONS Y) ; :: thesis:
thus rng h = F ; :: thesis:
thus for d being set st d in {} (PARTITIONS Y) holds
h . d in d ; :: thesis:
x = Y by A1, TARSKI:def 1;
hence x = Intersect F by SETFAM_1:def 9; :: thesis:
thus x <> {} by A1, TARSKI:def 1; :: thesis:

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:
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:

end;

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