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

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