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