consider A being non empty set , Z, u being Element of A, t being TriOp of A;
take TernaryFieldStr(# A,Z,u,t #) ; :: thesis: not TernaryFieldStr(# A,Z,u,t #) is empty
thus not the carrier of TernaryFieldStr(# A,Z,u,t #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum