let L be Lattice; :: thesis: for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt L,[#p,q#] is C_Lattice
let p, q be Element of L; :: thesis: ( L is C_Lattice & L is modular & p [= q implies latt L,[#p,q#] is C_Lattice )
assume A1: ( L is C_Lattice & L is modular & p [= q ) ; :: thesis: latt L,[#p,q#] is C_Lattice
then reconsider K = latt L,[#p,q#] as bounded Lattice by Th84;
K is complemented

proof

let b' 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 b'
reconsider b = b' as Element of L by Th69;
consider a being Element of L such that
A2: a is_a_complement_of b by A1, LATTICES:def 19;
A3: ( a "\/" b = Top L & a "/\" b = Bottom L ) by A2, LATTICES:def 18;
a "/\" q [= q by LATTICES:23;
then A4: ( p [= p "\/" (a "/\" q) & p "\/" (a "/\" q) [= q & H₁(K) = [#p,q#] ) by A1, Th73, FILTER_0:6, LATTICES:22;
then reconsider a' = p "\/" (a "/\" q) as Element of K by A1, Th63;
take a' ; :: thesis: a' is_a_complement_of b'
A5: ( b [= q & p [= b ) by A1, A4, Th63;
thus a' "\/" b' = (p "\/" (a "/\" q)) "\/" b by Th74
.= (b "\/" p) "\/" (a "/\" q) by LATTICES:def 5
.= b "\/" (a "/\" q) by A5, LATTICES:def 3
.= (Top L) "/\" q by A1, A3, A5, LATTICES:def 12
.= q by A1, LATTICES:43
.= Top K by A1, Th84 ; :: 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 )
thus a' "/\" b' = (p "\/" (a "/\" q)) "/\" b by Th74
.= p "\/" ((a "/\" q) "/\" b) by A1, A5, LATTICES:def 12
.= p "\/" (q "/\" (Bottom L)) by A3, LATTICES:def 7
.= p "\/" (Bottom L) by A1, LATTICES:40
.= p by A1, LATTICES:39
.= Bottom K by A1, Th84 ; :: thesis: b' "/\" a' = Bottom K
hence b' "/\" a' = Bottom K ; :: thesis: verum

end;

hence latt L,[#p,q#] is C_Lattice ; :: thesis: verum