let L be Lattice; :: thesis: for p being Element of L st L is C_Lattice & L is modular holds
latt (L,(.p.>) is C_Lattice
let p be Element of L; :: thesis: ( L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is modular ; :: thesis: latt (L,(.p.>) is C_Lattice
reconsider K = latt (L,(.p.>) as bounded Lattice by A1, Th83;
K is complemented

proof

let b9 be Element of K; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of K st b₁ is_a_complement_of b9
reconsider b = b9 as Element of L by Th69;
consider a being Element of L such that
A3: a is_a_complement_of b by A1, LATTICES:def 19;
A4: a "\/" b = Top L by A3, LATTICES:def 18;
A5: H₁(K) = (.p.> by Th73;
then A6: b [= p by Th29;
p "/\" a [= p by LATTICES:6;
then reconsider a9 = p "/\" a as Element of K by A5, Th29;
take a9 ; :: thesis: a9 is_a_complement_of b9
thus a9 "\/" b9 = (p "/\" a) "\/" b by Th74
.= (b "\/" a) "/\" p by A2, A6, LATTICES:def 12
.= p by A1, A4, LATTICES:17
.= Top K by Th81 ; :: according to LATTICES:def 18 :: thesis: ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
hence b9 "\/" a9 = Top K ; :: thesis: ( a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
A7: a "/\" b = Bottom L by A3, LATTICES:def 18;
thus a9 "/\" b9 = (p "/\" a) "/\" b by Th74
.= p "/\" (Bottom L) by A7, LATTICES:def 7
.= Bottom L by A1, LATTICES:15
.= Bottom K by A1, Th82 ; :: thesis: b9 "/\" a9 = Bottom K
hence b9 "/\" a9 = Bottom K ; :: thesis: verum

end;

hence latt (L,(.p.>) is C_Lattice ; :: thesis: verum