let X be non empty set ; :: thesis: for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
let FS be non empty Subset of (Filters X); :: thesis: ( FS is c=-linear implies union FS is Filter of X )
assume A1: FS is c=-linear ; :: thesis: union FS is Filter of X
A2: for S being set st S in FS holds
S c= bool X

proof

let S be set ; :: thesis: ( S in FS implies S c= bool X )
assume A3: S in FS ; :: thesis: S c= bool X
S is Element of Filters X by A3;
hence S c= bool X ; :: thesis: verum

end;

consider S being set such that
A4: S in FS by XBOOLE_0:def 1;
S is Filter of X by A4, Th15;
then X in S by Th5;
then A5: union FS is non empty Subset-Family of X by A2, A4, TARSKI:def 4, ZFMISC_1:94;
A6: not {} in union FS

proof

assume {} in union FS ; :: thesis: contradiction
then consider S being set such that
A7: {} in S and
A8: S in FS by TARSKI:def 4;
S is Filter of X by A8, Th15;
hence contradiction by A7, Def1; :: thesis: verum

end;

for Y1, Y2 being Subset of X holds
( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )

proof

let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
thus ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) :: thesis: ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS )

proof

assume A9: ( Y1 in union FS & Y2 in union FS ) ; :: thesis: Y1 /\ Y2 in union FS
then consider S1 being set such that
A10: Y1 in S1 and
A11: S1 in FS by TARSKI:def 4;
consider S2 being set such that
A12: Y2 in S2 and
A13: S2 in FS by A9, TARSKI:def 4;
A14: ( S1 is Filter of X & S2 is Filter of X ) by A11, A13, Th15;
A15: S1,S2 are_c=-comparable by A1, A11, A13, ORDINAL1:def 9;

per cases ( S1 c= S2 or S2 c= S1 ) by A15, XBOOLE_0:def 9;

suppose S1 c= S2 ; :: thesis: Y1 /\ Y2 in union FS

then Y1 /\ Y2 in S2 by A10, A12, A14, Def1;
hence Y1 /\ Y2 in union FS by A13, TARSKI:def 4; :: thesis: verum

end;

suppose S2 c= S1 ; :: thesis: Y1 /\ Y2 in union FS

then Y1 /\ Y2 in S1 by A10, A12, A14, Def1;
hence Y1 /\ Y2 in union FS by A11, TARSKI:def 4; :: thesis: verum

end;

end;

end;

assume A16: ( Y1 in union FS & Y1 c= Y2 ) ; :: thesis: Y2 in union FS
then consider S1 being set such that
A17: Y1 in S1 and
A18: S1 in FS by TARSKI:def 4;
S1 is Filter of X by A18, Th15;
then Y2 in S1 by A16, A17, Def1;
hence Y2 in union FS by A18, TARSKI:def 4; :: thesis: verum

end;

hence union FS is Filter of X by A5, A6, Def1; :: thesis: verum