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 )

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

hence
PA '<' '\/' G
by SETFAM_1:def 2; :: thesis: verum
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

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

end;( 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

hence
ex b being set st
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;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

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