let S be Language; :: thesis:
let D be RuleSet of S; :: thesis:
let X be functional set ; :: thesis:
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); :: thesis:
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 ) ; :: thesis:
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 )

let a, b be set ; :: thesis:
assume a in Y ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
( ((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; :: thesis:
thus c in Y ; :: thesis:

end;