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