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