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

assume a in Y ; :: thesis:
then consider X being set such that
A3: ( a in X & X in Z ) by TARSKI:def 4;
thus contradiction by A1, A3, Th19; :: thesis:

end;

consider X being Element of Z;
X in (SF_have b) \ (SF_have a) by A1, TARSKI:def 3;
then A4: b in X by Th19;
then A5: b in Y by A1, TARSKI:def 4;
reconsider Y = Y as non empty Subset of L by A1, A4, TARSKI:def 4;
Y is Filter of L

let p, q be Element of L; :: according to FILTER_0:def 1 :: 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
A6: ( p in X1 & X1 in Z ) by TARSKI:def 4;
assume q in Y ; :: thesis:
then consider X2 being set such that
A7: ( q in X2 & X2 in Z ) by TARSKI:def 4;
A8: ( X1,X2 are_c=-comparable & X1 is Filter of L & X2 is Filter of L ) by A1, A6, A7, Th19, ORDINAL1:def 9;
then ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9;
then ( p "/\" q in X1 or p "/\" q in X2 ) by A6, A7, A8, FILTER_0:def 1;
hence p "/\" q in Y by A6, A7, TARSKI:def 4; :: thesis:

end;

assume p "/\" q in Y ; :: thesis:
then consider X1 being set such that
A9: ( p "/\" q in X1 & X1 in Z ) by TARSKI:def 4;
X1 is Filter of L by A1, A9, Th19;
then ( p in X1 & q in X1 ) by A9, FILTER_0:def 1;
hence ( p in Y & q in Y ) by A9, TARSKI:def 4; :: thesis:

end;

hence Y in (SF_have b) \ (SF_have a) by A2, A5, 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:92; :: thesis: