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