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