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

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

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

end;

hence u = Top L by RLSUB_2:65; :: thesis: verum