let R, S be non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr ; :: thesis: ( the carrier of R /\ the carrier of S is non empty directed lower Subset of S implies Bottom S in the carrier of R )
assume A1: the carrier of R /\ the carrier of S is non empty directed lower Subset of S ; :: thesis: Bottom S in the carrier of R
then consider x being object such that
A2: x in the carrier of R /\ the carrier of S by XBOOLE_0:def 1;
reconsider x = x as Element of S by A2, Th13;
Bottom S <= x by YELLOW_0:44;
then Bottom S in the carrier of R /\ the carrier of S by A1, A2, WAYBEL_0:def 19;
hence Bottom S in the carrier of R by XBOOLE_0:def 4; :: thesis: verum