let L be strict Lattice; :: thesis: latt <.L.) = L
dom the L_meet of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def 1;
then A1: the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68;
dom the L_join of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def 1;
then the L_join of L = the L_join of L || the carrier of L by RELAT_1:68;
hence latt <.L.) = L by A1, Def9; :: thesis: verum