theorem Th32: :: LATTAD_1:26

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