let L be Lattice; :: thesis: for F being Filter of L st L is modular holds
latt F is modular
let F be Filter of L; :: thesis: ( L is modular implies latt F 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 F is modular
let a, b, c be Element of (latt F); :: according to LATTICES:def 12 :: thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A2: a [= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
reconsider p = a, q = b, r = c as Element of F by Th63;
( b "/\" c = q "/\" r & a "\/" b = p "\/" q ) by Th64;
then ( a "\/" (b "/\" c) = p "\/" (q "/\" r) & (a "\/" b) "/\" c = (p "\/" q) "/\" r & p [= r ) by A2, Th64, Th65;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1; :: thesis: verum