( dom (ThetaOrder L) = the carrier of L & rng (ThetaOrder L) = the carrier of L ) by Th32;
hence ThetaOrder L is Relation of the carrier of L by RELSET_1:4; :: thesis: verum