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 ) )
assume A2: a in PA ; :: thesis: ex b being set st
( b in '\/' G & a c= b )
then A3: ( a c= Y & a <> {} ) by EQREL_1:def 6;
consider x being Element of a;
A4: x in Y by A3, TARSKI:def 3;
union ('\/' G) = Y by EQREL_1:def 6;
then consider b being set such that
A5: ( x in b & b in '\/' G ) by A4, TARSKI:def 4;
b is_upper_min_depend_of G by A1, A5, Def3;
then b is_a_dependent_set_of PA by A1, Def2;
then consider B being set such that
A6: ( B c= PA & B <> {} & b = union B ) by PARTIT1:def 1;
a in B

proof

consider u being set such that
A7: ( x in u & u in B ) by A5, A6, TARSKI:def 4;
a /\ u <> {} by A3, A7, XBOOLE_0:def 4;
then A8: not a misses u by XBOOLE_0:def 7;
u in PA by A6, A7;
hence a in B by A2, A7, A8, EQREL_1:def 6; :: thesis: verum

end;

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

end;

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