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, Th81;
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 Th68;
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;
A5: H₁(K) = (.p.> by Th72;
then A6: b [= p by Th28;
p "/\" a [= p by LATTICES:6;
then reconsider a9 = p "/\" a as Element of K by A5, Th28;
take a9 ; :: thesis: a9 is_a_complement_of b9
thus a9 "\/" b9 = (p "/\" a) "\/" b by Th73
.= (b "\/" a) "/\" p by A2, A6
.= p by A1, A4
.= Top K by Th79 ; :: 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;
thus a9 "/\" b9 = (p "/\" a) "/\" b by Th73
.= p "/\" (Bottom L) by A7, LATTICES:def 7
.= Bottom L by A1
.= Bottom K by A1, Th80 ; :: thesis: b9 "/\" a9 = Bottom K
hence b9 "/\" a9 = Bottom K ; :: thesis: verum

end;

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