let X, Y be set ; :: thesis: for R being Relation st X misses Y holds
(R | X) | Y = {}
let R be Relation; :: thesis: ( X misses Y implies (R | X) | Y = {} )
assume X misses Y ; :: thesis: (R | X) | Y = {}
then X /\ Y = {} by XBOOLE_0:def 7;
hence (R | X) | Y = R | {} by Th100
.= {} ;
:: thesis: verum