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 a being set st a in PA holds
ex b being set st
( b in '\/' G & a c= b )
proof
let a be set ; :: thesis: ( a in PA implies ex b being set st
( b in '\/' G & a c= b ) )

set x = the Element of a;
A2: union ('\/' G) = Y by EQREL_1:def 4;
assume A3: a in PA ; :: thesis: ex b being set st
( b in '\/' G & a c= b )

then A4: a <> {} by EQREL_1:def 4;
then the Element of a in Y by ;
then consider b being set such that
A5: the Element of a in b and
A6: b in '\/' G by ;
b is_upper_min_depend_of G by A1, A6, Def3;
then consider B being set such that
A7: B c= PA and
B <> {} and
A8: b = union B by ;
a in B
proof
consider u being set such that
A9: the Element of a in u and
A10: u in B by ;
A11: a /\ u <> {} by ;
u in PA by ;
hence a in B by ; :: thesis: verum
end;
hence ex b being set st
( b in '\/' G & a c= b ) by ; :: thesis: verum
end;
hence PA '<' '\/' G by SETFAM_1:def 2; :: thesis: verum