let X, S be non empty set ; :: thesis: for R being Relation of X st R is irreflexive & field R c= S holds
R is_irreflexive_in S
let R be Relation of X; :: thesis: ( R is irreflexive & field R c= S implies R is_irreflexive_in S )
assume A1: ( R is irreflexive & field R c= S ) ; :: thesis: R is_irreflexive_in S
then A2: R is_irreflexive_in field R by RELAT_2:def 10;
let x be set ; :: according to RELAT_2:def 2 :: thesis: ( not x in S or not [x,x] in R )
assume A3: x in S ; :: thesis: not [x,x] in R
S = (field R) \/ (S \ (field R)) by A1, XBOOLE_1:45;
then A4: ( not x in S or x in field R or x in S \ (field R) ) by XBOOLE_0:def 3;
( x in S \ (field R) implies not [x,x] in R )

proof

assume x in S \ (field R) ; :: thesis: not [x,x] in R
then x in S \ ((dom R) \/ (rng R)) by RELAT_1:def 6;
then x in (S \ (dom R)) /\ (S \ (rng R)) by XBOOLE_1:53;
then ( x in S \ (dom R) & x in S \ (rng R) ) by XBOOLE_0:def 4;
then ( x in S & not x in dom R & not x in rng R ) by XBOOLE_0:def 5;
hence not [x,x] in R by RELAT_1:def 5; :: thesis: verum

end;

hence not [x,x] in R by A2, A3, A4, RELAT_2:def 2; :: thesis: verum