let L be Lattice; :: thesis: for F being Filter of L st L is distributive holds
latt F is distributive
let F be Filter of L; :: thesis: ( L is distributive implies latt F is distributive )
assume A1: for p, q, r being Element of L holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) ; :: according to LATTICES:def 11 :: thesis: latt F is distributive
let p', q', r' be Element of (latt F); :: according to LATTICES:def 11 :: thesis: p' "/\" (q' "\/" r') = (p' "/\" q') "\/" (p' "/\" r')
reconsider p = p', q = q', r = r', qr = q' "\/" r' as Element of F by Th63;
A2: ( p' "/\" q' = p "/\" q & p' "/\" r' = p "/\" r ) by Th64;
thus p' "/\" (q' "\/" r') = p "/\" qr by Th64
.= p "/\" (q "\/" r) by Th64
.= (p "/\" q) "\/" (p "/\" r) by A1
.= (p' "/\" q') "\/" (p' "/\" r') by A2, Th64 ; :: thesis: verum