let L be transitive antisymmetric with_infima lower-bounded RelStr ; :: thesis: for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds
a "/\" c = Bottom L
let a, b, c be Element of L; :: thesis: ( a <= b & b "/\" c = Bottom L implies a "/\" c = Bottom L )
assume ( a <= b & b "/\" c = Bottom L ) ; :: thesis: a "/\" c = Bottom L
then A1: a "/\" c <= Bottom L by Th6;
Bottom L <= a "/\" c by YELLOW_0:44;
hence a "/\" c = Bottom L by A1, YELLOW_0:def 3; :: thesis: verum