let L be RelStr ; :: thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds

X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ) holds

for X being Subset of L st X = union A holds

X is filtered

let A be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in A holds

X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds

X is filtered )

assume that

A1: for X being Subset of L st X in A holds

X is filtered and

A2: for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ; :: thesis: for X being Subset of L st X = union A holds

X is filtered

let Z be Subset of L; :: thesis: ( Z = union A implies Z is filtered )

assume A3: Z = union A ; :: thesis: Z is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in Z & y in Z implies ex z being Element of L st

( z in Z & z <= x & z <= y ) )

assume x in Z ; :: thesis: ( not y in Z or ex z being Element of L st

( z in Z & z <= x & z <= y ) )

then consider X being set such that

A4: x in X and

A5: X in A by A3, TARSKI:def 4;

assume y in Z ; :: thesis: ex z being Element of L st

( z in Z & z <= x & z <= y )

then consider Y being set such that

A6: y in Y and

A7: Y in A by A3, TARSKI:def 4;

reconsider X = X, Y = Y as Subset of L by A5, A7;

consider W being Subset of L such that

A8: W in A and

A9: X \/ Y c= W by A2, A5, A7;

A10: X c= X \/ Y by XBOOLE_1:7;

A11: Y c= X \/ Y by XBOOLE_1:7;

A12: x in X \/ Y by A4, A10;

A13: y in X \/ Y by A6, A11;

W is filtered by A1, A8;

then consider z being Element of L such that

A14: z in W and

A15: x >= z and

A16: y >= z by A9, A12, A13;

take z ; :: thesis: ( z in Z & z <= x & z <= y )

thus ( z in Z & z <= x & z <= y ) by A3, A8, A14, A15, A16, TARSKI:def 4; :: thesis: verum

X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ) holds

for X being Subset of L st X = union A holds

X is filtered

let A be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in A holds

X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds

X is filtered )

assume that

A1: for X being Subset of L st X in A holds

X is filtered and

A2: for X, Y being Subset of L st X in A & Y in A holds

ex Z being Subset of L st

( Z in A & X \/ Y c= Z ) ; :: thesis: for X being Subset of L st X = union A holds

X is filtered

let Z be Subset of L; :: thesis: ( Z = union A implies Z is filtered )

assume A3: Z = union A ; :: thesis: Z is filtered

let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( x in Z & y in Z implies ex z being Element of L st

( z in Z & z <= x & z <= y ) )

assume x in Z ; :: thesis: ( not y in Z or ex z being Element of L st

( z in Z & z <= x & z <= y ) )

then consider X being set such that

A4: x in X and

A5: X in A by A3, TARSKI:def 4;

assume y in Z ; :: thesis: ex z being Element of L st

( z in Z & z <= x & z <= y )

then consider Y being set such that

A6: y in Y and

A7: Y in A by A3, TARSKI:def 4;

reconsider X = X, Y = Y as Subset of L by A5, A7;

consider W being Subset of L such that

A8: W in A and

A9: X \/ Y c= W by A2, A5, A7;

A10: X c= X \/ Y by XBOOLE_1:7;

A11: Y c= X \/ Y by XBOOLE_1:7;

A12: x in X \/ Y by A4, A10;

A13: y in X \/ Y by A6, A11;

W is filtered by A1, A8;

then consider z being Element of L such that

A14: z in W and

A15: x >= z and

A16: y >= z by A9, A12, A13;

take z ; :: thesis: ( z in Z & z <= x & z <= y )

thus ( z in Z & z <= x & z <= y ) by A3, A8, A14, A15, A16, TARSKI:def 4; :: thesis: verum