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