set A = the non empty set ;
set P = the Relation of the non empty set ,( the non empty set *);
take DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) ; :: thesis: ( not DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty & DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict )
thus not the carrier of DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty ; :: according to STRUCT_0:def 1 :: thesis: DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict
thus DTConstrStr(# the non empty set , the Relation of the non empty set ,( the non empty set *) #) is strict ; :: thesis: verum