let L be non empty meet-associative meet-absorbing join-absorbing LattStr ; :: thesis: for a, b, c being Element of L st a [= b holds
a "/\" c [= b "/\" c
let a, b, c be Element of L; :: thesis: ( a [= b implies a "/\" c [= b "/\" c )
assume a [= b ; :: thesis: a "/\" c [= b "/\" c
hence (a "/\" c) "\/" (b "/\" c) = ((a "/\" b) "/\" c) "\/" (b "/\" c) by Th2
.= (a "/\" (b "/\" c)) "\/" (b "/\" c) by Def7
.= b "/\" c by Def8 ;
:: according to LATTICES:def 3 :: thesis: verum