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