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 ;
set x = the Element of a;
A5: the Element of a in Y by ;
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 ;
a c= b by ;
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 ;
set u = the Element of a;
A10: the Element of a = x by ;
A11: the Element of a in Y by ;
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 ;
a c= b by ;
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 ; :: thesis: verum