consider A being non empty set , R being Relation4 of A;
take ParStr(# A,R #) ; :: thesis: not ParStr(# A,R #) is empty
thus not the carrier of ParStr(# A,R #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum