let L be Lattice; :: thesis: ( L is C_Lattice iff L .: is C_Lattice )
A1: ( ( L is bounded implies ( L is lower-bounded & L is upper-bounded ) ) & ( L is lower-bounded & L is upper-bounded implies L is bounded ) & ( L .: is bounded implies ( L .: is lower-bounded & L .: is upper-bounded ) ) & ( L .: is lower-bounded & L .: is upper-bounded implies L .: is bounded ) & ( L is lower-bounded implies L .: is upper-bounded ) & ( L .: is upper-bounded implies L is lower-bounded ) & ( L is upper-bounded implies L .: is lower-bounded ) & ( L .: is lower-bounded implies L is upper-bounded ) ) by LATTICE2:63, LATTICE2:64;
thus ( L is C_Lattice implies L .: is C_Lattice ) :: thesis: ( L .: is C_Lattice implies L is C_Lattice )

proof

assume A2: L is C_Lattice ; :: thesis: L .: is C_Lattice

now

let p' be Element of (L .: ); :: thesis: ex r being Element of (L .: ) st r is_a_complement_of p'
consider q being Element of L such that
A3: q is_a_complement_of .: p' by A2, LATTICES:def 19;
take r = q .: ; :: thesis: r is_a_complement_of p'
( L is lower-bounded & L is upper-bounded & .: (q .: ) = q & q "\/" (.: p') = Top L & q "/\" (.: p') = Bottom L ) by A2, A3, LATTICES:def 18;
then ( (q .: ) "/\" p' = Top L & (q .: ) "\/" p' = Bottom L & Top (L .: ) = Bottom L & Bottom (L .: ) = Top L ) by LATTICE2:78, LATTICE2:79;
hence r is_a_complement_of p' by LATTICES:def 18; :: thesis: verum

end;

hence L .: is C_Lattice by A1, A2, LATTICES:def 19; :: thesis: verum

end;

assume A4: L .: is C_Lattice ; :: thesis: L is C_Lattice

now

let p be Element of L; :: thesis: ex r being Element of L st r is_a_complement_of p
consider q' being Element of (L .: ) such that
A5: q' is_a_complement_of p .: by A4, LATTICES:def 19;
take r = .: q'; :: thesis: r is_a_complement_of p
( L is lower-bounded & L is upper-bounded & .: (p .: ) = p & q' "\/" (p .: ) = Top (L .: ) & q' "/\" (p .: ) = Bottom (L .: ) ) by A4, A5, LATTICE2:63, LATTICE2:64, LATTICES:def 18;
then ( (.: q') "/\" p = Top (L .: ) & (.: q') "\/" p = Bottom (L .: ) & Top (L .: ) = Bottom L & Bottom (L .: ) = Top L ) by LATTICE2:78, LATTICE2:79;
hence r is_a_complement_of p by LATTICES:def 18; :: thesis: verum

end;

hence L is C_Lattice by A1, A4, LATTICES:def 19; :: thesis: verum