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