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