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