let L be GAD_Lattice; :: thesis: ( L is join-commutative iff LatRelStr L is directed )
thus ( L is join-commutative implies LatRelStr L is directed ) :: thesis: ( LatRelStr L is directed implies L is join-commutative )

proof

assume A1: L is join-commutative ; :: thesis: LatRelStr L is directed
set X = [#] (LatRelStr L);
for x, y being Element of (LatRelStr L) st x in [#] (LatRelStr L) & y in [#] (LatRelStr L) holds
ex z being Element of (LatRelStr L) st
( z in [#] (LatRelStr L) & x <= z & y <= z )

proof

let x, y be Element of (LatRelStr L); :: thesis: ( x in [#] (LatRelStr L) & y in [#] (LatRelStr L) implies ex z being Element of (LatRelStr L) st
( z in [#] (LatRelStr L) & x <= z & y <= z ) )
assume ( x in [#] (LatRelStr L) & y in [#] (LatRelStr L) ) ; :: thesis: ex z being Element of (LatRelStr L) st
( z in [#] (LatRelStr L) & x <= z & y <= z )
reconsider xx = x, yy = y as Element of L ;
xx "\/" yy = yy "\/" xx by A1;
then consider z being Element of L such that
B1: ( xx [= z & yy [= z ) by Th3823, LemX3;
reconsider zz = z as Element of (LatRelStr L) ;
C1: x <= zz by OrdLat, ORDERS_2:def 5, B1;
y <= zz by OrdLat, ORDERS_2:def 5, B1;
hence ex z being Element of (LatRelStr L) st
( z in [#] (LatRelStr L) & x <= z & y <= z ) by C1; :: thesis: verum

end;

hence LatRelStr L is directed by WAYBEL_0:def 6, WAYBEL_0:def 1; :: thesis: verum

end;

assume a1: LatRelStr L is directed ; :: thesis: L is join-commutative
for a, b being Element of L holds a "\/" b = b "\/" a

proof

let a, b be Element of L; :: thesis: a "\/" b = b "\/" a
reconsider aa = a, bb = b as Element of (LatRelStr L) ;
set X = [#] (LatRelStr L);
consider z being Element of (LatRelStr L) such that
B2: ( z in [#] (LatRelStr L) & aa <= z & bb <= z ) by WAYBEL_0:def 1, a1, WAYBEL_0:def 6;
reconsider zz = z as Element of L ;
B3: a [= zz by B2, OrdLat, ORDERS_2:def 5;
b [= zz by B2, OrdLat, ORDERS_2:def 5;
hence a "\/" b = b "\/" a by DefB2, B3; :: thesis: verum

end;

hence L is join-commutative ; :: thesis: verum