let L be D_Lattice; :: thesis:
let a, b be Element of L; :: thesis:
let Z be set ; :: thesis:
assume that
A1: Z <> {} and
A2: Z c= (SF_have b) \ (SF_have a) and
A3: Z is c=-linear ; :: thesis:
reconsider Z = Z as Subset-Family of L by A2, XBOOLE_1:1;
take Y = union Z; :: thesis:
Y in (SF_have b) \ (SF_have a)

set X = the Element of Z;
A4: not a in Y

assume a in Y ; :: thesis:
then ex X being set st
( a in X & X in Z ) by TARSKI:def 4;
hence contradiction by A2, Th17; :: thesis:

end;

the Element of Z in (SF_have b) \ (SF_have a) by A1, A2;
then A5: b in the Element of Z by Th17;
then A6: b in Y by A1, TARSKI:def 4;
reconsider Y = Y as non empty Subset of L by A1, A5, TARSKI:def 4;

let p, q be Element of L; :: thesis:
thus ( p in Y & q in Y implies p "/\" q in Y ) :: thesis:

assume p in Y ; :: thesis:
then consider X1 being set such that
A7: p in X1 and
A8: X1 in Z by TARSKI:def 4;
A9: X1 is Filter of L by A2, A8, Th17;
assume q in Y ; :: thesis:
then consider X2 being set such that
A10: q in X2 and
A11: X2 in Z by TARSKI:def 4;
X1,X2 are_c=-comparable by A3, A8, A11, ORDINAL1:def 8;
then A12: ( X1 c= X2 or X2 c= X1 ) ;
X2 is Filter of L by A2, A11, Th17;
then ( p "/\" q in X1 or p "/\" q in X2 ) by A7, A10, A9, A12, FILTER_0:8;
hence p "/\" q in Y by A8, A11, TARSKI:def 4; :: thesis:

end;

assume p "/\" q in Y ; :: thesis:
then consider X1 being set such that
A13: p "/\" q in X1 and
A14: X1 in Z by TARSKI:def 4;
A15: X1 is Filter of L by A2, A14, Th17;
then A16: q in X1 by A13, FILTER_0:8;
p in X1 by A13, A15, FILTER_0:8;
hence ( p in Y & q in Y ) by A14, A16, TARSKI:def 4; :: thesis:

end;

then Y is Filter of L by FILTER_0:8;
hence Y in (SF_have b) \ (SF_have a) by A4, A6, Lm1; :: thesis:

end;

hence ( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by ZFMISC_1:74; :: thesis: