take L ; :: thesis: ( the carrier of L c= 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 )
thus ( the carrier of L c= 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 ) ; :: thesis: verum