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 directed ) & ( 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 directed
let A be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in A holds
X is directed ) & ( 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 directed )
assume that
A1: for X being Subset of L st X in A holds
X is directed 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 directed
let Z be Subset of L; :: thesis: ( Z = union A implies Z is directed )
assume A3: Z = union A ; :: thesis: Z is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in Z & y in Z implies ex z being Element of L st
( z in Z & x <= z & y <= z ) )
assume x in Z ; :: thesis: ( not y in Z or ex z being Element of L st
( z in Z & x <= z & y <= z ) )
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 & x <= z & y <= z )
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 directed ) by A1, A6;
then consider z being Element of L such that
A7: ( z in W & x <= z & y <= z ) by Def1;
take z ; :: thesis: ( z in Z & x <= z & y <= z )
thus ( z in Z & x <= z & y <= z ) by A3, A6, A7, TARSKI:def 4; :: thesis: verum