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