let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; :: thesis: for a, b, c being Element of L st a [= b & a [= c holds
a [= b "/\" c
let a, b, c be Element of L; :: thesis: ( a [= b & a [= c implies a [= b "/\" c )
a "/\" a = a ;
hence ( a [= b & a [= c implies a [= b "/\" c ) by Th5; :: thesis: verum