let Y be non empty set ; :: thesis:
let PA be a_partition of Y; :: thesis:
A1: {Y} is Subset-Family of Y by ZFMISC_1:68;
A2: union {Y} = Y by ZFMISC_1:25;
for A being Subset of Y st A in {Y} holds
( A <> {} & ( for B being Subset of Y holds
( not B in {Y} or A = B or A misses B ) ) )

end;

then A5: {Y} is a_partition of Y by A1, A2, EQREL_1:def 4;
for a being set st a in PA holds
ex b being set st
( b in {Y} & a c= b )

let a be set ; :: thesis:
assume A6: a in PA ; :: thesis:
then A7: a <> {} by EQREL_1:def 4;
set x = the Element of a;
the Element of a in Y by A6, A7, TARSKI:def 3;
then consider b being set such that
the Element of a in b and
A8: b in {Y} by A2, TARSKI:def 4;
b = Y by A8, TARSKI:def 1;
hence ex b being set st
( b in {Y} & a c= b ) by A6, A8; :: thesis:

end;