take A = 1-sorted(# the infinite set #); :: thesis: ( A is strict & not A is finite )
thus A is strict ; :: thesis: not A is finite
thus not the carrier of A is finite ; :: according to STRUCT_0:def 11 :: thesis: verum