consider A being non trivial set ;
take RelStr(# A,(Total A) #) ; :: thesis: ( not RelStr(# A,(Total A) #) is diagonal & not RelStr(# A,(Total A) #) is empty )
thus ( not RelStr(# A,(Total A) #) is diagonal & not RelStr(# A,(Total A) #) is empty ) ; :: thesis: verum