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