let S, R be Relation; :: thesis: ( ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) & ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R ) )
thus ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) :: thesis: ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R )

proof

assume ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} ) ; :: thesis: CL S = CL R
then ( CL S c= CL R & CL R c= CL S ) by Th58;
hence CL S = CL R by XBOOLE_0:def 10; :: thesis: verum

end;

assume ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} ) ; :: thesis: CL S = CL R
then ( CL S c= CL R & CL R c= CL S ) by Th58;
hence CL S = CL R by XBOOLE_0:def 10; :: thesis: verum