theorem Th32: :: LATWAL_2:28

for L being WA_Lattice holds
( dom (LatOrder L) = the carrier of L & rng (LatOrder L) = the carrier of L & field (LatOrder L) = the carrier of L )