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 :: thesis: for j being Element of I holds j "\/" (i => i) = i => i

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

end;

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