take the non empty strict flat Poset ; :: thesis: ( the non empty strict flat Poset is strict & not the non empty strict flat Poset is empty & the non empty strict flat Poset is flat & the non empty strict flat Poset is chain-complete )
thus ( the non empty strict flat Poset is strict & not the non empty strict flat Poset is empty & the non empty strict flat Poset is flat & the non empty strict flat Poset is chain-complete ) by Lemflat02; :: thesis: verum