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