let L be Lattice; :: thesis: for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds
u = Bottom L
let u be Element of L; :: thesis: ( ( for v being Element of L holds u "\/" v = v ) implies u = Bottom L )
assume A1: for v being Element of L holds u "\/" v = v ; :: thesis: u = Bottom L

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

let v be Element of L; :: thesis: v "/\" u = u
v "\/" u = v by A1;
then u [= v ;
hence v "/\" u = u by LATTICES:4; :: thesis: verum

end;

hence u = Bottom L by RLSUB_2:64; :: thesis: verum