let L be D_Lattice; :: thesis: for F being Filter of L
for a, b being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let F be Filter of L; :: thesis: for a, b being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let a, b be Element of L; :: thesis: ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
( F in (SF_have b) \ (SF_have a) iff ( F in SF_have b & not F in SF_have a ) ) by XBOOLE_0:def 5;
hence ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) ) by Th16; :: thesis: verum