ex R being strict RelStr st
( the carrier of R = X & R is real ) by Th1;
hence ex b₁ being strict real RelStr st the carrier of b₁ = X ; :: thesis: verum