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 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 A3, TARSKI:def 3;
then consider b being set such that
A5: the Element of a in b and
A6: b in '\/' G by A2, TARSKI:def 4;
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 A1, PARTIT1:def 1;
a in B

proof

consider u being set such that
A9: the Element of a in u and
A10: u in B by A5, A8, TARSKI:def 4;
A11: a /\ u <> {} by A4, A9, XBOOLE_0:def 4;
u in PA by A7, A10;
hence a in B by A3, A10, A11, EQREL_1:def 4, XBOOLE_0:def 7; :: thesis: verum

end;

hence ex b being set st
( b in '\/' G & a c= b ) by A6, A8, ZFMISC_1:74; :: thesis: verum

end;

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