set A = the non empty set ;
set C = the Relation of [: the non empty set , the non empty set :];
take ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) ; :: thesis: not ParOrtStr(# the non empty set , the Relation of [: the non empty set , the non empty set :], the Relation of [: the non empty set , the non empty set :] #) is empty
thus not the carrier of ParOrtStr(# the non empty set , the Relation of [: the non empty set , 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