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 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 & x <= z & y <= z )
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 directed 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 & x <= z & y <= z )
thus ( z in Z & x <= z & y <= z ) by A3, A8, A14, A15, A16, TARSKI:def 4; :: thesis: verum