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

end;

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