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