let L be 1_Lattice; :: thesis: Top L = Bottom (L .:)
reconsider u = Top L as Element of (L .:) ;

now :: thesis: for v being Element of (L .:) holds v "/\" u = u

let v be Element of (L .:); :: thesis: v "/\" u = u
reconsider v9 = v as Element of L ;
thus v "/\" u = (Top L) "\/" v9 by Th37
.= u ; :: thesis: verum

end;

hence Top L = Bottom (L .:) by RLSUB_2:64; :: thesis: verum