let X be set ; :: thesis: for R being Relation holds
( R .: X = {} iff dom R misses X )
let R be Relation; :: thesis: ( R .: X = {} iff dom R misses X )
set y = the Element of R .: X;
thus ( R .: X = {} implies dom R misses X ) :: thesis: ( dom R misses X implies R .: X = {} )
proof
assume A1: R .: X = {} ; :: thesis: dom R misses X
assume not dom R misses X ; :: thesis: contradiction
then consider x being object such that
A2: x in dom R and
A3: x in X by XBOOLE_0:3;
ex y being object st [x,y] in R by A2, XTUPLE_0:def 12;
hence contradiction by A1, A2, A3, Th104; :: thesis: verum
end;
assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def 7 :: thesis: R .: X = {}
assume not R .: X = {} ; :: thesis: contradiction
then ex x being object st
( x in dom R & [x, the Element of R .: X] in R & x in X ) by Th104;
hence contradiction by A4, XBOOLE_0:def 4; :: thesis: verum