LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is Lattice-like
proof
thus
( ( for
p,
q being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
p "\/" q = q "\/" p ) & ( for
p,
q,
r being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
p "\/" (q "\/" r) = (p "\/" q) "\/" r ) & ( for
p,
q being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
(p "/\" q) "\/" q = q ) & ( for
p,
q being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
p "/\" q = q "/\" p ) & ( for
p,
q,
r being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
p "/\" (q "/\" r) = (p "/\" q) "/\" r ) & ( for
p,
q being
Element of
LattStr(#
(Funcs A,REAL ),
(maxfuncreal A),
(minfuncreal A) #) holds
p "/\" (p "\/" q) = p ) )
by Th20, Th21, Th22, Th23, Th26, Th28;
:: according to LATTICES:def 4,
LATTICES:def 5,
LATTICES:def 6,
LATTICES:def 7,
LATTICES:def 8,
LATTICES:def 9,
LATTICES:def 10 :: thesis: verum
end;
hence
LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is strict Lattice
; :: thesis: verum