take id X ; :: thesis: ( id X is symmetric & not id X is irreflexive & not id X is empty )
thus ( id X is symmetric & not id X is irreflexive & not id X is empty ) ; :: thesis: verum