let L be Lattice; :: thesis: for p being Element of L st L is C_Lattice & L is modular holds
latt L,(.p.> is C_Lattice
let p be Element of L; :: thesis: ( L is C_Lattice & L is modular implies latt L,(.p.> is C_Lattice )
assume A1:
( L is C_Lattice & L is modular )
; :: thesis: latt L,(.p.> is C_Lattice
then reconsider K = latt L,(.p.> as bounded Lattice by Th83;
K is complemented
proof
let b' be
Element of
K;
:: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of K st b1 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;
A4:
(
p "/\" a [= p &
H1(
K)
= (.p.> )
by Th73, LATTICES:23;
then reconsider a' =
p "/\" a as
Element of
K by Th29;
take
a'
;
:: thesis: a' is_a_complement_of b'
A5:
b [= p
by A4, Th29;
thus a' "\/" b' =
(p "/\" a) "\/" b
by Th74
.=
(b "\/" a) "/\" p
by A1, A5, LATTICES:def 12
.=
p
by A1, A3, 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 )
thus a' "/\" b' =
(p "/\" a) "/\" b
by Th74
.=
p "/\" (Bottom L)
by A3, 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