e is subexpression of e by Th33;
hence ex b₁ being subexpression of e st b₁ is constructor ; :: thesis: verum