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_sup_of {x,y},
L &
"\/" (
{x,y},
L)
in the
carrier of
S holds
(
ex_sup_of {x,y},
S &
"\/" (
{x,y},
S)
= "\/" (
{x,y},
L) )
by Th64;