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