let L be Lattice; :: thesis: ( L is C_Lattice iff L .: is C_Lattice )
A1: ( L is upper-bounded iff L .: is lower-bounded ) by LATTICE2:49;
A2: ( L is lower-bounded iff L .: is upper-bounded ) by LATTICE2:48;
thus ( L is C_Lattice implies L .: is C_Lattice ) :: thesis: ( L .: is C_Lattice implies L is C_Lattice )

proof

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

now :: thesis: for p9 being Element of (L .:) ex r being Element of (L .:) st r is_a_complement_of p9

let p9 be Element of (L .:); :: thesis: ex r being Element of (L .:) st r is_a_complement_of p9
consider q being Element of L such that
A4: q is_a_complement_of .: p9 by A3, LATTICES:def 19;
take r = q .: ; :: thesis: r is_a_complement_of p9
q "\/" (.: p9) = Top L by A4;
then A5: (q .:) "/\" p9 = Top L ;
q "/\" (.: p9) = Bottom L by A4;
then A6: (q .:) "\/" p9 = Bottom L ;
( Top (L .:) = Bottom L & Bottom (L .:) = Top L ) by A3, LATTICE2:61, LATTICE2:62;
hence r is_a_complement_of p9 by A5, A6; :: thesis: verum

end;

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

end;

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

now :: thesis: for p being Element of L ex r being Element of L st r is_a_complement_of p

let p be Element of L; :: thesis: ex r being Element of L st r is_a_complement_of p
consider q9 being Element of (L .:) such that
A8: q9 is_a_complement_of p .: by A7, LATTICES:def 19;
q9 "\/" (p .:) = Top (L .:) by A8;
then A9: (.: q9) "/\" p = Top (L .:) ;
take r = .: q9; :: thesis: r is_a_complement_of p
L is upper-bounded by A7, LATTICE2:49;
then A10: Bottom (L .:) = Top L by LATTICE2:62;
q9 "/\" (p .:) = Bottom (L .:) by A8;
then A11: (.: q9) "\/" p = Bottom (L .:) ;
L is lower-bounded by A7, LATTICE2:48;
then Top (L .:) = Bottom L by LATTICE2:61;
hence r is_a_complement_of p by A9, A11, A10; :: thesis: verum

end;

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