theorem
for
L being non
empty transitive RelStr for
S being non
empty full SubRelStr of
L for
x,
y being
Element of
S st
ex_inf_of {x,y},
L &
"/\" (
{x,y},
L)
in the
carrier of
S holds
(
ex_inf_of {x,y},
S &
"/\" (
{x,y},
S)
= "/\" (
{x,y},
L) )
by Th63;