set L = LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #);
for p, q, r being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r by Th22;
then A1: LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is join-associative by LATTICES:def 5;
for p, q being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds (p "/\" q) "\/" q = q by Th26;
then A2: LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is meet-absorbing by LATTICES:def 8;
for p, q being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds p "/\" (p "\/" q) = p by Th28;
then A3: LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is join-absorbing by LATTICES:def 9;
for p, q, r being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r by Th23;
then A4: LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is meet-associative by LATTICES:def 7;
for p, q being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds p "/\" q = q "/\" p by Th21;
then A5: LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is meet-commutative by LATTICES:def 6;
for p, q being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds p "\/" q = q "\/" p by Th20;
then LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is join-commutative by LATTICES:def 4;
hence LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is strict Lattice by A1, A2, A5, A4, A3; :: thesis: verum