theorem Th32: :: LATTAD_1:28

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