let L be D_Lattice; :: thesis: for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let b, a be Element of L; :: thesis: for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let x be set ; :: thesis: ( x in (SF_have b) \ (SF_have a) implies ( x is Filter of L & b in x & not a in x ) )
assume x in (SF_have b) \ (SF_have a) ; :: thesis: ( x is Filter of L & b in x & not a in x )
then ( x in SF_have b & not x in SF_have a ) by XBOOLE_0:def 5;
then ( x is Filter of L & b in x & ( not x is Filter of L or not a in x ) ) by Th18;
hence ( x is Filter of L & b in x & not a in x ) ; :: thesis: verum