let L be D_Lattice; :: thesis: for a, b 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 a, b 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 A1: x in (SF_have b) \ (SF_have a) ; :: thesis: ( x is Filter of L & b in x & not a in x )
then A2: not x in SF_have a by XBOOLE_0:def 5;
A3: x in SF_have b by A1, XBOOLE_0:def 5;
then x is Filter of L by Th16;
hence ( x is Filter of L & b in x & not a in x ) by A3, A2, Th16; :: thesis: verum