let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; :: thesis: for a, b, c, d being Element of L st a [= b & c [= d holds
a "/\" c [= b "/\" d
let a, b, c, d be Element of L; :: thesis: ( a [= b & c [= d implies a "/\" c [= b "/\" d )
assume a [= b ; :: thesis: ( not c [= d or a "/\" c [= b "/\" d )
then A1: a "/\" b = a by LATTICES:4;
assume c [= d ; :: thesis: a "/\" c [= b "/\" d
then a "/\" c = (a "/\" b) "/\" (c "/\" d) by A1, LATTICES:4
.= ((a "/\" b) "/\" c) "/\" d by LATTICES:def 7
.= (b "/\" (a "/\" c)) "/\" d by LATTICES:def 7
.= (a "/\" c) "/\" (b "/\" d) by LATTICES:def 7 ;
hence a "/\" c [= b "/\" d by LATTICES:4; :: thesis: verum