let Y be non empty set ; :: thesis: for PA being a_partition of Y holds

( %O Y '>' PA & PA '>' %I Y )

let PA be a_partition of Y; :: thesis: ( %O Y '>' PA & PA '>' %I Y )

A1: for a being set st a in PA holds

ex b being set st

( b in %O Y & a c= b )

ex b being set st

( b in PA & a c= b )

( %O Y '>' PA & PA '>' %I Y )

let PA be a_partition of Y; :: thesis: ( %O Y '>' PA & PA '>' %I Y )

A1: for a being set st a in PA holds

ex b being set st

( b in %O Y & a c= b )

proof

for a being set st a in %I Y holds
let a be set ; :: thesis: ( a in PA implies ex b being set st

( b in %O Y & a c= b ) )

assume A2: a in PA ; :: thesis: ex b being set st

( b in %O Y & a c= b )

then A3: a c= Y ;

A4: a <> {} by A2, EQREL_1:def 4;

set x = the Element of a;

A5: the Element of a in Y by A2, A4, TARSKI:def 3;

union (%O Y) = Y by EQREL_1:def 4;

then consider b being set such that

the Element of a in b and

A6: b in %O Y by A5, TARSKI:def 4;

a c= b by A3, A6, TARSKI:def 1;

hence ex b being set st

( b in %O Y & a c= b ) by A6; :: thesis: verum

end;( b in %O Y & a c= b ) )

assume A2: a in PA ; :: thesis: ex b being set st

( b in %O Y & a c= b )

then A3: a c= Y ;

A4: a <> {} by A2, EQREL_1:def 4;

set x = the Element of a;

A5: the Element of a in Y by A2, A4, TARSKI:def 3;

union (%O Y) = Y by EQREL_1:def 4;

then consider b being set such that

the Element of a in b and

A6: b in %O Y by A5, TARSKI:def 4;

a c= b by A3, A6, TARSKI:def 1;

hence ex b being set st

( b in %O Y & a c= b ) by A6; :: thesis: verum

ex b being set st

( b in PA & a c= b )

proof

hence
( %O Y '>' PA & PA '>' %I Y )
by A1, SETFAM_1:def 2; :: thesis: verum
let a be set ; :: thesis: ( a in %I Y implies ex b being set st

( b in PA & a c= b ) )

assume A7: a in %I Y ; :: thesis: ex b being set st

( b in PA & a c= b )

then a in { {x} where x is Element of Y : verum } by EQREL_1:37;

then consider x being Element of Y such that

A8: a = {x} ;

A9: a <> {} by A7, EQREL_1:def 4;

set u = the Element of a;

A10: the Element of a = x by A8, TARSKI:def 1;

A11: the Element of a in Y by A7, A9, TARSKI:def 3;

union PA = Y by EQREL_1:def 4;

then consider b being set such that

A12: the Element of a in b and

A13: b in PA by A11, TARSKI:def 4;

a c= b by A8, A10, A12, TARSKI:def 1;

hence ex b being set st

( b in PA & a c= b ) by A13; :: thesis: verum

end;( b in PA & a c= b ) )

assume A7: a in %I Y ; :: thesis: ex b being set st

( b in PA & a c= b )

then a in { {x} where x is Element of Y : verum } by EQREL_1:37;

then consider x being Element of Y such that

A8: a = {x} ;

A9: a <> {} by A7, EQREL_1:def 4;

set u = the Element of a;

A10: the Element of a = x by A8, TARSKI:def 1;

A11: the Element of a in Y by A7, A9, TARSKI:def 3;

union PA = Y by EQREL_1:def 4;

then consider b being set such that

A12: the Element of a in b and

A13: b in PA by A11, TARSKI:def 4;

a c= b by A8, A10, A12, TARSKI:def 1;

hence ex b being set st

( b in PA & a c= b ) by A13; :: thesis: verum