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