let L be non empty meet-absorbing join-absorbing LattStr ; :: thesis: for a, b being Element of L holds
( a [= b iff a "/\" b = a )
let a, b be Element of L; :: thesis: ( a [= b iff a "/\" b = a )
( a [= b iff a "\/" b = b ) by Def3;
hence ( a [= b iff a "/\" b = a ) by Def8, Def9; :: thesis: verum