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 )
A3: a c= Y by A2;
A4: a <> {} by A2, EQREL_1:def 6;
consider x being Element of a;
A5: x in Y by A2, A4, TARSKI:def 3;
A6: union (%O Y) = Y by EQREL_1:def 6;
consider b being set such that
x in b and
A7: b in %O Y by A5, A6, TARSKI:def 4;
A8: a c= b by A3, A7, TARSKI:def 1;
thus ex b being set st
( b in %O Y & a c= b ) by A7, A8; :: thesis: verum

end;

A9: 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 )
A11: a in { {x} where x is Element of Y : verum } by A10, EQREL_1:46;
consider x being Element of Y such that
A12: a = {x} by A11;
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;
A16: union PA = Y by EQREL_1:def 6;
consider b being set such that
A17: u in b and
A18: b in PA by A15, A16, TARSKI:def 4;
A19: a c= b

proof

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

end;

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

end;

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