take {} T ; :: thesis: {} T c= Int (Cl (Int ({} T)))
thus {} T c= Int (Cl (Int ({} T))) by XBOOLE_1:2; :: thesis: verum