let f be Function; :: thesis: for A, B being set st A misses B holds
f " A misses f " B
let A, B be set ; :: thesis: ( A misses B implies f " A misses f " B )
assume A misses B ; :: thesis: f " A misses f " B
then A /\ B = {} by XBOOLE_0:def 7;
then {} = f " (A /\ B) by RELAT_1:136
.= (f " A) /\ (f " B) by Th137 ;
hence f " A misses f " B by XBOOLE_0:def 7; :: thesis: verum