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 & 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
A5: ( y in Y & Y in A ) by A3, TARSKI:def 4;
reconsider X = X, Y = Y as Subset of L by A4, A5;
consider W being Subset of L such that
A6: ( W in A & X \/ Y c= W ) by A2, A4, A5;
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( x in X \/ Y & y in X \/ Y ) by A4, A5;
then ( x in W & y in W & W is filtered ) by A1, A6;
then consider z being Element of L such that
A7: ( z in W & x >= z & y >= z ) by Def2;
take z ; :: thesis: ( z in Z & z <= x & z <= y )
thus ( z in Z & z <= x & z <= y ) by A3, A6, A7, TARSKI:def 4; :: thesis: verum