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:64;
A2: ( L is lower-bounded iff L .: is upper-bounded ) by LATTICE2:63;
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

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, LATTICES:def 18;
then A5: (q .: ) "/\" p9 = Top L ;
q "/\" (.: p9) = Bottom L by A4, LATTICES:def 18;
then A6: (q .: ) "\/" p9 = Bottom L ;
( Top (L .: ) = Bottom L & Bottom (L .: ) = Top L ) by A3, LATTICE2:78, LATTICE2:79;
hence r is_a_complement_of p9 by A5, A6, LATTICES:def 18; :: 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

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, LATTICES:def 18;
then A9: (.: q9) "/\" p = Top (L .: ) ;
take r = .: q9; :: thesis: r is_a_complement_of p
L is upper-bounded by A7, LATTICE2:64;
then A10: Bottom (L .: ) = Top L by LATTICE2:79;
q9 "/\" (p .: ) = Bottom (L .: ) by A8, LATTICES:def 18;
then A11: (.: q9) "\/" p = Bottom (L .: ) ;
L is lower-bounded by A7, LATTICE2:63;
then Top (L .: ) = Bottom L by LATTICE2:78;
hence r is_a_complement_of p by A9, A11, A10, LATTICES:def 18; :: thesis: verum

end;

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