let L be Lattice; :: thesis: ( L is upper-bounded iff L .: is lower-bounded )
thus ( L is upper-bounded implies L .: is lower-bounded ) :: thesis: ( L .: is lower-bounded implies L is upper-bounded )

proof

given c being Element of L such that A1: for a being Element of L holds
( c "\/" a = c & a "\/" c = c ) ; :: according to LATTICES:def 14 :: thesis: L .: is lower-bounded
reconsider c9 = c as Element of (L .:) ;
take c9 ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (L .:) holds
( c9 "/\" b₁ = c9 & b₁ "/\" c9 = c9 )
let a9 be Element of (L .:); :: thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L ;
thus c9 "/\" a9 = c "\/" a
.= c9 by A1 ; :: thesis: a9 "/\" c9 = c9
hence a9 "/\" c9 = c9 ; :: thesis: verum

end;

given c being Element of (L .:) such that A2: for a being Element of (L .:) holds
( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def 13 :: thesis: L is upper-bounded
reconsider c9 = c as Element of L ;
take c9 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of L holds
( c9 "\/" b₁ = c9 & b₁ "\/" c9 = c9 )
let a9 be Element of L; :: thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
reconsider a = a9 as Element of (L .:) ;
thus c9 "\/" a9 = c "/\" a
.= c9 by A2 ; :: thesis: a9 "\/" c9 = c9
hence a9 "\/" c9 = c9 ; :: thesis: verum