consider D being non empty set , f being Function of D,(bool (bool D));
take FMT_Space_Str(# D,f #) ; :: thesis: ( not FMT_Space_Str(# D,f #) is empty & FMT_Space_Str(# D,f #) is strict )
thus not the carrier of FMT_Space_Str(# D,f #) is empty ; :: according to STRUCT_0:def 1 :: thesis: FMT_Space_Str(# D,f #) is strict
thus FMT_Space_Str(# D,f #) is strict ; :: thesis: verum