take 1-sorted(# {{}} #) ; :: thesis: ( 1-sorted(# {{}} #) is strict & not 1-sorted(# {{}} #) is empty )
thus 1-sorted(# {{}} #) is strict ; :: thesis: not 1-sorted(# {{}} #) is empty
thus not the carrier of 1-sorted(# {{}} #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum