let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y st PA in G holds
PA '>' '/\' G
let G be Subset of (PARTITIONS Y); :: thesis: for PA being a_partition of Y st PA in G holds
PA '>' '/\' G
let PA be a_partition of Y; :: thesis: ( PA in G implies PA '>' '/\' G )
assume A1: PA in G ; :: thesis: PA '>' '/\' G
for x being set st x in '/\' G holds
ex a being set st
( a in PA & x c= a )

proof

let x be set ; :: thesis: ( x in '/\' G implies ex a being set st
( a in PA & x c= a ) )
assume x in '/\' G ; :: thesis: ex a being set st
( a in PA & x c= a )
then consider h being Function, F being Subset-Family of Y such that
A2: dom h = G and
A3: rng h = F and
A4: for d being set st d in G holds
h . d in d and
A5: x = Intersect F and
x <> {} by Def1;
set a = h . PA;
A6: h . PA in PA by A1, A4;
A7: h . PA in rng h by A1, A2, FUNCT_1:def 3;
then Intersect F = meet F by A3, SETFAM_1:def 9;
hence ex a being set st
( a in PA & x c= a ) by A3, A5, A6, A7, SETFAM_1:3; :: thesis: verum

end;

hence PA '>' '/\' G by SETFAM_1:def 2; :: thesis: verum