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