let L be Lattice; 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; ( 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
; 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;
LATTICES:def 19 ex b1 being Element of the carrier of K st b1 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:
H1(
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
;
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
;
LATTICES:def 18 ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
hence
b9 "\/" a9 = Top K
;
( 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
;
b9 "/\" a9 = Bottom K
hence
b9 "/\" a9 = Bottom K
;
verum
end;
hence
latt (L,[#p,q#]) is C_Lattice
; verum