set L = the non empty complete Poset;
take the non empty complete Poset ; :: thesis: the non empty complete Poset is complete
thus the non empty complete Poset is complete ; :: thesis: verum