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