set A = the non empty strict complete Poset;
take the non empty strict complete Poset ; :: thesis: ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty )
thus ( the non empty strict complete Poset is complete & the non empty strict complete Poset is with_suprema & the non empty strict complete Poset is with_infima & the non empty strict complete Poset is strict & not the non empty strict complete Poset is empty ) by Th12; :: thesis: verum