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 6;
consider x being Element of a;
A5: x in Y by A2, A4, TARSKI:def 3;
union (%O Y) = Y by EQREL_1:def 6;
then consider b being set such that
x in b and
A7: b in %O Y by A5, TARSKI:def 4;
a c= b by A3, A7, TARSKI:def 1;
hence ex b being set st
( b in %O Y & a c= b ) by A7; :: 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 A10: 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:46;
then consider x being Element of Y such that
A12: a = {x} ;
A13: a <> {} by A10, EQREL_1:def 6;
consider u being Element of a;
A14: u = x by A12, TARSKI:def 1;
A15: u in Y by A10, A13, TARSKI:def 3;
union PA = Y by EQREL_1:def 6;
then consider b being set such that
A17: u in b and
A18: b in PA by A15, TARSKI:def 4;
a c= b

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in a or x1 in b )
assume x1 in a ; :: thesis: x1 in b
hence x1 in b by A12, A14, A17, TARSKI:def 1; :: thesis: verum

end;

hence ex b being set st
( b in PA & a c= b ) by A18; :: thesis: verum

end;

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