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