let L be transitive antisymmetric with_suprema with_infima lower-bounded RelStr ; :: thesis: for a, b, c being Element of L st a meets b "/\" c holds
a meets b
let a, b, c be Element of L; :: thesis: ( a meets b "/\" c implies a meets b )
assume A1: a meets b "/\" c ; :: thesis: a meets b
assume A2: not a meets b ; :: thesis: contradiction
a "/\" (b "/\" c) = (a "/\" b) "/\" c by LATTICE3:16
.= (Bottom L) "/\" c by A2
.= Bottom L by Th25 ;
hence contradiction by A1; :: thesis: verum