T is full infs-inheriting sups-inheriting SubRelStr of T by Th13;
hence ex b₁ being CLSubFrame of st b₁ is complete ; :: thesis: verum