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

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