let L be 1_Lattice; :: thesis: for a being Element of holds (Top L) "/\" a = a
let a be Element of ; :: thesis: (Top L) "/\" a = a
thus (Top L) "/\" a = ((Top L) "\/" a) "/\" a by Def17
.= a by Def9 ; :: thesis: verum