let L be non empty LattStr ; :: thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-idempotent & L is join-idempotent ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: ( L is meet-idempotent & L is join-idempotent )
A2: for x being Element of L holds x "\/" x = x
proof
let a be Element of L; :: thesis: a "\/" a = a
a = a "\/" (a "/\" a) by A1;
hence a "\/" a = a by A1; :: thesis: verum
end;
for x being Element of L holds x "/\" x = x
proof
let a be Element of L; :: thesis: a "/\" a = a
a = a "/\" (a "\/" a) by A1;
hence a "/\" a = a by A1; :: thesis: verum
end;
hence ( L is meet-idempotent & L is join-idempotent ) by A2, ROBBINS1:def 7, SHEFFER1:def 9; :: thesis: verum