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