set X = the infinite set ;
take CofinTop the infinite set ; :: thesis: ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober )
thus ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober ) ; :: thesis: verum