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 that
A1: L is C_Lattice and
A2: L is modular and
A3: p [= q ; :: thesis: latt (L,[#p,q#]) is C_Lattice
reconsider K = latt (L,[#p,q#]) as bounded Lattice by A3, Th82;
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
A4: a is_a_complement_of b by A1, LATTICES:def 19;
A5: a "/\" b = Bottom L by A4;
A6: a "\/" b = Top L by A4;
A7: H₁(K) = [#p,q#] by Th72;
then A8: b [= q by A3, Th62;
a "/\" q [= q by LATTICES:6;
then ( p [= p "\/" (a "/\" q) & p "\/" (a "/\" q) [= q ) by A3, FILTER_0:6, LATTICES:5;
then reconsider a9 = p "\/" (a "/\" q) as Element of K by A3, A7, Th62;
take a9 ; :: thesis: a9 is_a_complement_of b9
A9: p [= b by A3, A7, Th62;
thus a9 "\/" b9 = (p "\/" (a "/\" q)) "\/" b by Th73
.= (b "\/" p) "\/" (a "/\" q) by LATTICES:def 5
.= b "\/" (a "/\" q) by A9
.= (Top L) "/\" q by A2, A6, A8
.= q by A1
.= Top K by A3, Th82 ; :: 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 )
thus a9 "/\" b9 = (p "\/" (a "/\" q)) "/\" b by Th73
.= p "\/" ((a "/\" q) "/\" b) by A2, A9
.= p "\/" (q "/\" (Bottom L)) by A5, LATTICES:def 7
.= p "\/" (Bottom L) by A1
.= p by A1
.= Bottom K by A3, Th82 ; :: thesis: b9 "/\" a9 = Bottom K
hence b9 "/\" a9 = Bottom K ; :: thesis: verum

end;

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