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