let S be Language; for D being RuleSet of S
for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
rng ((D,num) addw X) is c=directed
let D be RuleSet of S; for X being functional set
for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
rng ((D,num) addw X) is c=directed
let X be functional set ; for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds
rng ((D,num) addw X) is c=directed
set L = LettersOf S;
set F = S -firstChar ;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set EF = ExFormulasOf S;
let num be sequence of (ExFormulasOf S); ( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent implies rng ((D,num) addw X) is c=directed )
set f = (D,num) addw X;
reconsider Y = rng ((D,num) addw X) as non empty set ;
A1:
dom ((D,num) addw X) = NAT
by FUNCT_2:def 1;
assume A2:
( D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent )
; rng ((D,num) addw X) is c=directed
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 ;
( a in Y & b in Y implies ex c being set st
( a \/ b c= c & c in Y ) )
assume
a in Y
;
( 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) addw X) &
a = ((D,num) addw X) . x )
by FUNCT_1:def 3;
assume
b in Y
;
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) addw X) &
b = ((D,num) addw 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) addw X) . N as
Element of
rng ((D,num) addw X) by A1, FUNCT_1:def 3;
take
c
;
( a \/ b c= c & c in Y )
(
((D,num) addw X) . mm c= ((D,num) addw X) . (mm + nn) &
((D,num) addw X) . nn c= ((D,num) addw X) . (nn + mm) )
by Th17, A2;
hence
a \/ b c= c
by A3, A4, XBOOLE_1:8;
c in Y
thus
c in Y
;
verum
end;
hence
rng ((D,num) addw X) is c=directed
by COHSP_1:6; verum