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