consider P being non empty Poset;
set A = {P};
take {P} ; :: thesis: ( not {P} is empty & {P} is POSet_set-like )
for a being set st a in {P} holds
a is non empty Poset by TARSKI:def 1;
hence ( not {P} is empty & {P} is POSet_set-like ) by Def4; :: thesis: verum