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

now

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

end;

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