consider A being non empty set , a being Element of A;
take ZeroStr(# A,a #) ; :: thesis: ( ZeroStr(# A,a #) is strict & not ZeroStr(# A,a #) is empty )
thus ZeroStr(# A,a #) is strict ; :: thesis: not ZeroStr(# A,a #) is empty
thus not the carrier of ZeroStr(# A,a #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum