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