take InclPoset {{{} }} ; :: thesis: ( not InclPoset {{{} }} is empty & InclPoset {{{} }} is reflexive & InclPoset {{{} }} is transitive & InclPoset {{{} }} is antisymmetric & InclPoset {{{} }} is with_superior & InclPoset {{{} }} is with_comparable_down & InclPoset {{{} }} is strict )
thus ( not InclPoset {{{} }} is empty & InclPoset {{{} }} is reflexive & InclPoset {{{} }} is transitive & InclPoset {{{} }} is antisymmetric & InclPoset {{{} }} is with_superior & InclPoset {{{} }} is with_comparable_down & InclPoset {{{} }} is strict ) by Th1; :: thesis: verum