let X be set ; :: thesis: for R being Relation holds
( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X | R = id X ) )
let R be Relation; :: thesis: ( ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) & ( id X c= R & (R \ (id X)) * (id X) = {} implies X | R = id X ) )
thus ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) :: thesis: ( id X c= R & (R \ (id X)) * (id X) = {} implies X | R = id X )

proof

assume that
A1: id X c= R and
A2: (id X) * (R \ (id X)) = {} ; :: thesis: R | X = id X
R | X = (id X) * R by RELAT_1:94
.= (id X) * (R \/ (id X)) by A1, XBOOLE_1:12
.= (id X) * ((R \ (id X)) \/ (id X)) by XBOOLE_1:39
.= {} \/ ((id X) * (id X)) by A2, RELAT_1:51
.= id X by Th29 ;
hence R | X = id X ; :: thesis: verum

end;

thus ( id X c= R & (R \ (id X)) * (id X) = {} implies X | R = id X ) :: thesis: verum

proof

assume that
A3: id X c= R and
A4: (R \ (id X)) * (id X) = {} ; :: thesis: X | R = id X
X | R = R * (id X) by RELAT_1:123
.= (R \/ (id X)) * (id X) by A3, XBOOLE_1:12
.= ((R \ (id X)) \/ (id X)) * (id X) by XBOOLE_1:39
.= {} \/ ((id X) * (id X)) by A4, Th20
.= id X by Th29 ;
hence X | R = id X ; :: thesis: verum

end;