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) "/\" ('not' c) by LATTICE3:16
.= (Bottom L) "/\" ('not' c) by A2
.= Bottom L by Th25 ;
hence contradiction by A1; :: thesis: verum