let L be non empty LattRelStr ; :: thesis: ( L is join-associative & L is naturally_sup-generated implies L is transitive )
assume ( L is join-associative & L is naturally_sup-generated ) ; :: thesis: L is transitive
then reconsider L9 = L as non empty join-associative naturally_sup-generated LattRelStr ;
for x, y, z being Element of L9 st x <= y & y <= z holds
x <= z
proof
let x, y, z be Element of L9; :: thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( x [= y & y [= z ) by Th22;
then x [= z by LATTICES:7;
hence x <= z by Th22; :: thesis: verum
end;
hence L is transitive by YELLOW_0:def 2; :: thesis: verum