let I be I_Lattice; :: thesis: I is upper-bounded
consider i being Element of I;
take k = i => i; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of I holds
( k "\/" b₁ = k & b₁ "\/" k = k )
let j be Element of I; :: thesis: ( k "\/" j = k & j "\/" k = k )
i "/\" j [= i by LATTICES:23;
then ( j [= k & j "\/" k = k "\/" j ) by Def8;
hence ( k "\/" j = k & j "\/" k = k ) by LATTICES:def 3; :: thesis: verum