set A = the non empty set ;
set R = the Relation4 of the non empty set ;
take ParStr(# the non empty set , the Relation4 of the non empty set #) ; :: thesis: not ParStr(# the non empty set , the Relation4 of the non empty set #) is empty
thus not the carrier of ParStr(# the non empty set , the Relation4 of the non empty set #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum