let L be Lattice; :: thesis: for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
let p be Element of L; :: thesis: ( L is C_Lattice & L is M_Lattice implies latt <.p.) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is M_Lattice ; :: thesis: latt <.p.) is C_Lattice
reconsider B = L as C_Lattice by A1;
reconsider M = latt <.p.) as 01_Lattice by A1, Th58;
M is complemented

proof

let r9 be Element of M; :: according to LATTICES:def 19 :: thesis: ex b₁ being Element of the carrier of M st b₁ is_a_complement_of r9
reconsider r = r9 as Element of <.p.) by Th49;
reconsider p1 = p as Element of B ;
consider q being Element of L such that
A3: q is_a_complement_of r by A1, LATTICES:def 19;
the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider q9 = p "\/" q as Element of M by Th16;
take q9 ; :: thesis: q9 is_a_complement_of r9
thus q9 "\/" r9 = (p "\/" q) "\/" r by Th50
.= p "\/" (q "\/" r) by LATTICES:def 5
.= p1 "\/" (Top B) by A3
.= Top L
.= Top M by A1, Th57 ; :: according to LATTICES:def 18 :: thesis: ( r9 "\/" q9 = Top M & q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
hence r9 "\/" q9 = Top M ; :: thesis: ( q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
p [= r by Th15;
then (p "\/" q) "/\" r = p "\/" (q "/\" r) by A2, LATTICES:def 12;
hence q9 "/\" r9 = p "\/" (q "/\" r) by Th50
.= p1 "\/" (Bottom B) by A3
.= p
.= Bottom M by Th56 ;
:: thesis: r9 "/\" q9 = Bottom M
hence r9 "/\" q9 = Bottom M ; :: thesis: verum

end;

hence latt <.p.) is C_Lattice ; :: thesis: verum