set T = the non empty Hausdorff TopSpace;
take the non empty Hausdorff TopSpace ; :: thesis: the non empty Hausdorff TopSpace is sober
thus the non empty Hausdorff TopSpace is sober ; :: thesis: verum