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 Th69;
assume a9 [= c9 ; :: thesis: a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9
then A2: a [= c by Th75;
thus a9 "\/" (b9 "/\" c9) = a "\/" bc by Th74
.= a "\/" (b "/\" c) by Th74
.= (a "\/" b) "/\" c by A1, A2
.= ab "/\" c by Th74
.= (a9 "\/" b9) "/\" c9 by Th74 ; :: thesis: verum