let L be Lattice; :: thesis: for P being non empty ClosedSubset of L st L is modular holds
latt (L,P) is modular
let P be non empty ClosedSubset of L; :: thesis: ( L is modular implies latt (L,P) is modular )
assume A1: for a, b, c being Element of L st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def 12 :: thesis: latt (L,P) is modular
let a9, b9, c9 be Element of (latt (L,P)); :: according to LATTICES:def 12 :: thesis: ( not a9 [= c9 or a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9 )
reconsider a = a9, b = b9, c = c9, bc = b9 "/\" c9, ab = a9 "\/" b9 as Element of L by Th68;
assume a9 [= c9 ; :: thesis: a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9
then A2: a [= c by Th74;
thus a9 "\/" (b9 "/\" c9) = a "\/" bc by Th73
.= a "\/" (b "/\" c) by Th73
.= (a "\/" b) "/\" c by A1, A2
.= ab "/\" c by Th73
.= (a9 "\/" b9) "/\" c9 by Th73 ; :: thesis: verum