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