let L be Lattice; :: thesis: ( L is lower-bounded iff L .: is upper-bounded )
thus ( L is lower-bounded implies L .: is upper-bounded ) :: thesis: ( L .: is upper-bounded implies L is lower-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 13 :: thesis: L .: is upper-bounded
reconsider c' = c as Element of (L .: ) ;
take c' ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (L .: ) holds
( c' "\/" b₁ = c' & b₁ "\/" c' = c' )
let a' be Element of (L .: ); :: thesis: ( c' "\/" a' = c' & a' "\/" c' = c' )
reconsider a = a' as Element of L ;
thus c' "\/" a' = c "/\" a
.= c' by A1 ; :: thesis: a' "\/" c' = c'
hence a' "\/" c' = c' ; :: 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 14 :: thesis: L is lower-bounded
reconsider c' = c as Element of L ;
take c' ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of L holds
( c' "/\" b₁ = c' & b₁ "/\" c' = c' )
let a' be Element of L; :: thesis: ( c' "/\" a' = c' & a' "/\" c' = c' )
reconsider a = a' as Element of (L .: ) ;
thus c' "/\" a' = c "\/" a
.= c' by A2 ; :: thesis: a' "/\" c' = c'
hence a' "/\" c' = c' ; :: thesis: verum