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 x being set st x in '/\' G holds

ex a being set st

( a in PA & x c= a )

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 x being set st x in '/\' G holds

ex a being set st

( a in PA & x c= a )

proof

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

then Intersect F = meet F by A3, SETFAM_1:def 9;

hence ex a being set st

( a in PA & x c= a ) by A3, A5, A6, A7, SETFAM_1:3; :: thesis: verum

end;( 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 A1, A2, FUNCT_1:def 3;

then Intersect F = meet F by A3, SETFAM_1:def 9;

hence ex a being set st

( a in PA & x c= a ) by A3, A5, A6, A7, SETFAM_1:3; :: thesis: verum