let L be non empty LattRelStr ; :: thesis: ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated implies L is reflexive )
assume ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated ) ; :: thesis: L is reflexive
then reconsider L9 = L as non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated LattRelStr ;
for x being Element of L9 holds x <= x
proof
let x be Element of L9; :: thesis: x <= x
x [= x ;
hence x <= x by Th22; :: thesis: verum
end;
hence L is reflexive by YELLOW_0:def 1; :: thesis: verum