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 = {}
hence (R | X) | Y = R | {} by Th65
.= {} ;
:: thesis: verum