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;
( a in F0 or b in F0 ) by A3, A4, FILTER_0:def 5;
then ( F0 in (PrimeFilters L) . a or F0 in (PrimeFilters L) . b ) by A3, Th17;
hence x in ((PrimeFilters L) . a) \/ ((PrimeFilters L) . b) by A2, XBOOLE_0:def 3; :: 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 x in ((PrimeFilters L) . a) \/ ((PrimeFilters L) . b) ; :: thesis: x in (PrimeFilters L) . (a "\/" b)
then ( x in (PrimeFilters L) . a or x in (PrimeFilters L) . b ) by XBOOLE_0:def 3;
then ( ex F0 being Filter of L st
( x = F0 & F0 is prime & a in F0 ) or ex F0 being Filter of L st
( x = F0 & F0 is prime & b in F0 ) ) by Th17;
then consider F0 being Filter of L such that
A5: x = F0 and
A6: F0 is prime and
A7: ( a in F0 or b in F0 ) ;
a "\/" b in F0 by A6, A7, FILTER_0:def 5;
hence x in (PrimeFilters L) . (a "\/" b) by A5, A6, Th17; :: thesis: verum

end;

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