let L be non empty join-commutative join-associative 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: b = a "\/" b ;
assume c [= d ; :: thesis: a "\/" c [= b "\/" d
then b "\/" d = (a "\/" b) "\/" (c "\/" d) by A1
.= ((b "\/" a) "\/" c) "\/" d by LATTICES:def 5
.= (b "\/" (a "\/" c)) "\/" d by LATTICES:def 5
.= (a "\/" c) "\/" (b "\/" d) by LATTICES:def 5 ;
hence a "\/" c [= b "\/" d ; :: thesis: verum