take F = I --> (id a); :: thesis: doms F = I --> a
doms F = I --> (dom (id a)) by Th4;
hence doms F = I --> a ; :: thesis: verum