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