let S, X 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 that

A1: R is irreflexive and

A2: field R c= S ; :: thesis: R is_irreflexive_in S

let x be object ; :: according to RELAT_2:def 2 :: thesis: ( not x in S or not [x,x] in R )

S = (field R) \/ (S \ (field R)) by A2, XBOOLE_1:45;

then A3: ( not x in S or x in field R or x in S \ (field R) ) by XBOOLE_0:def 3;

A4: ( x in S \ (field R) implies not [x,x] in R )

hence ( not x in S or not [x,x] in R ) by A3, A4; :: thesis: verum

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 that

A1: R is irreflexive and

A2: field R c= S ; :: thesis: R is_irreflexive_in S

let x be object ; :: according to RELAT_2:def 2 :: thesis: ( not x in S or not [x,x] in R )

S = (field R) \/ (S \ (field R)) by A2, XBOOLE_1:45;

then A3: ( not x in S or x in field R or x in S \ (field R) ) by XBOOLE_0:def 3;

A4: ( x in S \ (field R) implies not [x,x] in R )

proof

R is_irreflexive_in field R
by A1;
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 \ (rng R) by XBOOLE_0:def 4;

then not x in rng R by XBOOLE_0:def 5;

hence not [x,x] in R by XTUPLE_0:def 13; :: thesis: verum

end;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 \ (rng R) by XBOOLE_0:def 4;

then not x in rng R by XBOOLE_0:def 5;

hence not [x,x] in R by XTUPLE_0:def 13; :: thesis: verum

hence ( not x in S or not [x,x] in R ) by A3, A4; :: thesis: verum