set A = the non empty set ;
set T = the Function of [: the non empty set ,I:], the non empty set ;
set o = the Function of the non empty set ,O;
set I = the Element of the non empty set ;
set F = the Subset of the non empty set ;
take S = Moore-SM_Final(# the non empty set , the Function of [: the non empty set ,I:], the non empty set , the Function of the non empty set ,O, the Element of the non empty set , the Subset of the non empty set #); :: thesis: ( not S is empty & S is strict )
thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: S is strict
thus S is strict ; :: thesis: verum