let L be 0_Lattice; :: thesis: Bottom L = Top (L .:)
reconsider u = Bottom 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 = (Bottom L) "/\" v9 by Th37
.= u ; :: thesis: verum

end;

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