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 st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def 12 :: thesis: latt L,P is modular
let a', b', c' be Element of ; :: according to LATTICES:def 12 :: thesis: ( not a' [= c' or a' "\/" (b' "/\" c') = (a' "\/" b') "/\" c' )
reconsider a = a', b = b', c = c', bc = b' "/\" c', ab = a' "\/" b' as Element of by Th69;
assume a' [= c' ; :: thesis: a' "\/" (b' "/\" c') = (a' "\/" b') "/\" c'
then A2: a [= c by Th75;
thus a' "\/" (b' "/\" c') = a "\/" bc by Th74
.= a "\/" (b "/\" c) by Th74
.= (a "\/" b) "/\" c by A1, A2
.= ab "/\" c by Th74
.= (a' "\/" b') "/\" c' by Th74 ; :: thesis: verum