let L be GAD_Lattice; :: thesis: ( L is join-commutative iff ThetaOrder L is being_partial-order )
set R = ThetaOrder L;
thus ( L is join-commutative implies ThetaOrder L is being_partial-order ) :: thesis: ( ThetaOrder L is being_partial-order implies L is join-commutative )
proof
assume L is join-commutative ; :: thesis: ThetaOrder L is being_partial-order
then ThetaOrder L is antisymmetric by Th31146;
hence ThetaOrder L is being_partial-order by ORDERS_1:def 5; :: thesis: verum
end;
assume ThetaOrder L is being_partial-order ; :: thesis: L is join-commutative
then ThetaOrder L is antisymmetric by ORDERS_1:def 5;
hence L is join-commutative by Th31146; :: thesis: verum