let I be I_Lattice; :: thesis: for i being Element of I holds i => i = Top I
let i be Element of I; :: thesis: i => i = Top I

now

let j be Element of I; :: thesis: j "\/" (i => i) = i => i
i "/\" j [= i by LATTICES:6;
then j [= i => i by Def8;
hence j "\/" (i => i) = i => i by LATTICES:def 3; :: thesis: verum

end;

hence i => i = Top I by RLSUB_2:65; :: thesis: verum