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