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

thus A is strict ; :: thesis: A is infinite

thus the carrier of A is infinite ; :: according to STRUCT_0:def 11 :: thesis: verum