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 & rng h = F ) and
A3: for d being set st d in G holds
h . d in d and
A4: ( x = Intersect F & x <> {} ) by Def1;
set a = h . PA;
A5: h . PA in PA by A1, A3;
A6: h . PA in rng h by A1, A2, FUNCT_1:def 5;
then Intersect F = meet F by A2, SETFAM_1:def 10;
hence ex a being set st
( a in PA & x c= a ) by A2, A4, A5, A6, SETFAM_1:4; :: thesis: verum

end;

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