let Y be non empty set ; :: thesis: for G being Subset of ()
for PA being a_partition of Y st PA in G holds
PA '>' '/\' G

let G be Subset of (); :: 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 ;
then Intersect F = meet F by ;
hence ex a being set st
( a in PA & x c= a ) by ; :: thesis: verum
end;
hence PA '>' '/\' G by SETFAM_1:def 2; :: thesis: verum