let L be 1_Lattice; :: thesis: for a being Element of L holds a [= Top L
let a be Element of L; :: thesis: a [= Top L
(Top L) "/\" a [= Top L by Th4;
hence a [= Top L ; :: thesis: verum