let L be Lattice; :: thesis: for p being Element of st L is C_Lattice & L is modular holds
latt L,(.p.> is C_Lattice
let p be Element of ; :: 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 b' be Element of ; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of K st b₁ is_a_complement_of b'
reconsider b = b' as Element of by Th69;
consider a being Element of 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:23;
then reconsider a' = p "/\" a as Element of by A5, Th29;
take a' ; :: thesis: a' is_a_complement_of b'
thus a' "\/" b' = (p "/\" a) "\/" b by Th74
.= (b "\/" a) "/\" p by A2, A6, LATTICES:def 12
.= p by A1, A4, LATTICES:43
.= Top K by Th81 ; :: according to LATTICES:def 18 :: thesis: ( b' "\/" a' = Top K & a' "/\" b' = Bottom K & b' "/\" a' = Bottom K )
hence b' "\/" a' = Top K ; :: thesis: ( a' "/\" b' = Bottom K & b' "/\" a' = Bottom K )
A7: a "/\" b = Bottom L by A3, LATTICES:def 18;
thus a' "/\" b' = (p "/\" a) "/\" b by Th74
.= p "/\" (Bottom L) by A7, LATTICES:def 7
.= Bottom L by A1, LATTICES:40
.= Bottom K by A1, Th82 ; :: thesis: b' "/\" a' = Bottom K
hence b' "/\" a' = Bottom K ; :: thesis: verum

end;

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