let X be set ; :: thesis: for S being Language
for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
rng ((D,num) AddFormulasTo X) is c=directed
let S be Language; :: thesis: for D being RuleSet of S
for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
rng ((D,num) AddFormulasTo X) is c=directed
let D be RuleSet of S; :: thesis: for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds
rng ((D,num) AddFormulasTo X) is c=directed
set FF = AllFormulasOf S;
let num be sequence of (AllFormulasOf S); :: thesis: ( D is isotone & R#1 S in D & R#8 S in D & X is D -consistent implies rng ((D,num) AddFormulasTo X) is c=directed )
set f = (D,num) AddFormulasTo X;
reconsider Y = rng ((D,num) AddFormulasTo X) as non empty set ;
assume A1: ( D is isotone & R#1 S in D & R#8 S in D & X is D -consistent ) ; :: thesis: rng ((D,num) AddFormulasTo X) is c=directed
A2: dom ((D,num) AddFormulasTo X) = NAT by FUNCT_2:def 1;
for a, b being set st a in Y & b in Y holds
ex c being set st
( a \/ b c= c & c in Y )

proof

let a, b be set ; :: thesis: ( a in Y & b in Y implies ex c being set st
( a \/ b c= c & c in Y ) )
assume a in Y ; :: thesis: ( not b in Y or ex c being set st
( a \/ b c= c & c in Y ) )
then consider x being object such that
A3: ( x in dom ((D,num) AddFormulasTo X) & a = ((D,num) AddFormulasTo X) . x ) by FUNCT_1:def 3;
assume b in Y ; :: thesis: ex c being set st
( a \/ b c= c & c in Y )
then consider y being object such that
A4: ( y in dom ((D,num) AddFormulasTo X) & b = ((D,num) AddFormulasTo X) . y ) by FUNCT_1:def 3;
reconsider mm = x, nn = y as Element of NAT by A3, A4;
reconsider N = mm + nn as Element of NAT by ORDINAL1:def 12;
reconsider c = ((D,num) AddFormulasTo X) . N as Element of Y by A2, FUNCT_1:def 3;
take c ; :: thesis: ( a \/ b c= c & c in Y )
( ((D,num) AddFormulasTo X) . mm c= ((D,num) AddFormulasTo X) . (mm + nn) & ((D,num) AddFormulasTo X) . nn c= ((D,num) AddFormulasTo X) . (nn + mm) ) by Lm72, A1;
hence a \/ b c= c by A3, A4, XBOOLE_1:8; :: thesis: c in Y
thus c in Y ; :: thesis: verum

end;

hence rng ((D,num) AddFormulasTo X) is c=directed by COHSP_1:6; :: thesis: verum