take {1} ; :: thesis: ( not {1} is empty & {1} is included_in_Seg )
thus ( not {1} is empty & {1} is included_in_Seg ) ; :: thesis: verum