set R = ThetaOrder L;
dom (ThetaOrder L) = the carrier of L by Th32;
hence for b₁ being Relation of the carrier of L st b₁ = ThetaOrder L holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum