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 )) #) ; :: thesis: ( 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 ; :: according to STRUCT_0:def 1 :: thesis: 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 ; :: thesis: verum