let L be distributive Lattice; :: thesis: for a, b being Element of L holds (PrimeFilters L) . (a "/\" b) = ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)
let a, b be Element of L; :: thesis: (PrimeFilters L) . (a "/\" b) = ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)
A1: (PrimeFilters L) . (a "/\" b) c= ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (PrimeFilters L) . (a "/\" b) or x in ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) )
set c = a "/\" b;
assume x in (PrimeFilters L) . (a "/\" b) ; :: thesis: x in ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b)
then consider F0 being Filter of L such that
A2: x = F0 and
A3: F0 is prime and
A4: a "/\" b in F0 by Th17;
A5: a in F0 by A4, FILTER_0:8;
A6: b in F0 by A4, FILTER_0:8;
A7: F0 in (PrimeFilters L) . a by A3, A5, Th17;
F0 in (PrimeFilters L) . b by A3, A6, Th17;
hence x in ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) by A2, A7, XBOOLE_0:def 4; :: thesis: verum

end;

((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) c= (PrimeFilters L) . (a "/\" b)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) or x in (PrimeFilters L) . (a "/\" b) )
assume A8: x in ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) ; :: thesis: x in (PrimeFilters L) . (a "/\" b)
then A9: x in (PrimeFilters L) . a by XBOOLE_0:def 4;
A10: x in (PrimeFilters L) . b by A8, XBOOLE_0:def 4;
A11: ex F0 being Filter of L st
( x = F0 & F0 is prime & a in F0 ) by A9, Th17;
ex F0 being Filter of L st
( x = F0 & F0 is prime & b in F0 ) by A10, Th17;
then consider F0 being Filter of L such that
A12: x = F0 and
A13: F0 is prime and
A14: a in F0 and
A15: b in F0 by A11;
a "/\" b in F0 by A14, A15, FILTER_0:8;
hence x in (PrimeFilters L) . (a "/\" b) by A12, A13, Th17; :: thesis: verum

end;

hence (PrimeFilters L) . (a "/\" b) = ((PrimeFilters L) . a) /\ ((PrimeFilters L) . b) by A1; :: thesis: verum