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

now

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

end;

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