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 )

proof

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;

for a being set st a in %I Y holds
ex b being set st
( b in PA & a c= b )

proof

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;

hence ( %O Y '>' PA & PA '>' %I Y ) by A1, SETFAM_1:def 2; :: thesis: verum