let L be RelStr ; :: thesis: for A being Subset-Family of st ( for X being Subset of st X in A holds
X is filtered ) & ( for X, Y being Subset of st X in A & Y in A holds
ex Z being Subset of st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of st X = union A holds
X is filtered
let A be Subset-Family of ; :: thesis: ( ( for X being Subset of st X in A holds
X is filtered ) & ( for X, Y being Subset of st X in A & Y in A holds
ex Z being Subset of st
( Z in A & X \/ Y c= Z ) ) implies for X being Subset of st X = union A holds
X is filtered )
assume that
A1: for X being Subset of st X in A holds
X is filtered and
A2: for X, Y being Subset of st X in A & Y in A holds
ex Z being Subset of st
( Z in A & X \/ Y c= Z ) ; :: thesis: for X being Subset of st X = union A holds
X is filtered
let Z be Subset of ; :: thesis: ( Z = union A implies Z is filtered )
assume A3: Z = union A ; :: thesis: Z is filtered
let x, y be Element of ; :: according to WAYBEL_0:def 2 :: thesis: ( x in Z & y in Z implies ex z being Element of st
( z in Z & z <= x & z <= y ) )
assume x in Z ; :: thesis: ( not y in Z or ex z being Element of 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 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 by A5, A7;
consider W being Subset of 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 such that
A14: z in W and
A15: x >= z and
A16: y >= z by A9, A12, A13, Def2;
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