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:65
.= (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:32
.= id X by Th12 ;
hence R | X = id X ; :: thesis: verum
end;
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:92
.= (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, Th6
.= id X by Th12 ;
hence X |` R = id X ; :: thesis: verum