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 )

A1: for S being set st S in FS holds

S c= bool X

A2: S in FS by XBOOLE_0:def 1;

assume A3: FS is c=-linear ; :: thesis: union FS is Filter of X

A4: 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 ) )

S is Filter of X by A2, Th15;

then X in S by Th5;

then union FS is non empty Subset-Family of X by A1, A2, TARSKI:def 4, ZFMISC_1:76;

hence union FS is Filter of X by A18, A4, Def1; :: thesis: verum

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 )

A1: for S being set st S in FS holds

S c= bool X

proof

consider S being object such that
let S be set ; :: thesis: ( S in FS implies S c= bool X )

assume S in FS ; :: thesis: S c= bool X

then S is Element of Filters X ;

hence S c= bool X ; :: thesis: verum

end;assume S in FS ; :: thesis: S c= bool X

then S is Element of Filters X ;

hence S c= bool X ; :: thesis: verum

A2: S in FS by XBOOLE_0:def 1;

assume A3: FS is c=-linear ; :: thesis: union FS is Filter of X

A4: 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

A18:
not {} in union FS
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 )

A14: Y1 in union FS and

A15: Y1 c= Y2 ; :: thesis: Y2 in union FS

consider S1 being set such that

A16: Y1 in S1 and

A17: S1 in FS by A14, TARSKI:def 4;

S1 is Filter of X by A17, Th15;

then Y2 in S1 by A15, A16, Def1;

hence Y2 in union FS by A17, TARSKI:def 4; :: thesis: verum

end;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 that
assume that

A5: Y1 in union FS and

A6: Y2 in union FS ; :: thesis: Y1 /\ Y2 in union FS

consider S1 being set such that

A7: Y1 in S1 and

A8: S1 in FS by A5, TARSKI:def 4;

A9: S1 is Filter of X by A8, Th15;

consider S2 being set such that

A10: Y2 in S2 and

A11: S2 in FS by A6, TARSKI:def 4;

A12: S1,S2 are_c=-comparable by A3, A8, A11;

A13: S2 is Filter of X by A11, Th15;

end;A5: Y1 in union FS and

A6: Y2 in union FS ; :: thesis: Y1 /\ Y2 in union FS

consider S1 being set such that

A7: Y1 in S1 and

A8: S1 in FS by A5, TARSKI:def 4;

A9: S1 is Filter of X by A8, Th15;

consider S2 being set such that

A10: Y2 in S2 and

A11: S2 in FS by A6, TARSKI:def 4;

A12: S1,S2 are_c=-comparable by A3, A8, A11;

A13: S2 is Filter of X by A11, Th15;

A14: Y1 in union FS and

A15: Y1 c= Y2 ; :: thesis: Y2 in union FS

consider S1 being set such that

A16: Y1 in S1 and

A17: S1 in FS by A14, TARSKI:def 4;

S1 is Filter of X by A17, Th15;

then Y2 in S1 by A15, A16, Def1;

hence Y2 in union FS by A17, TARSKI:def 4; :: thesis: verum

proof

reconsider S = S as set by TARSKI:1;
assume
{} in union FS
; :: thesis: contradiction

then consider S being set such that

A19: {} in S and

A20: S in FS by TARSKI:def 4;

S is Filter of X by A20, Th15;

hence contradiction by A19, Def1; :: thesis: verum

end;then consider S being set such that

A19: {} in S and

A20: S in FS by TARSKI:def 4;

S is Filter of X by A20, Th15;

hence contradiction by A19, Def1; :: thesis: verum

S is Filter of X by A2, Th15;

then X in S by Th5;

then union FS is non empty Subset-Family of X by A1, A2, TARSKI:def 4, ZFMISC_1:76;

hence union FS is Filter of X by A18, A4, Def1; :: thesis: verum