let L be non empty 1-sorted ; :: thesis: for R being total Relation of the carrier of L holds
( R is reflexive iff for x being Element of L holds [x,x] in R )
let R be total Relation of the carrier of L; :: thesis: ( R is reflexive iff for x being Element of L holds [x,x] in R )
thus ( R is reflexive implies for x being Element of L holds [x,x] in R ) :: thesis: ( ( for x being Element of L holds [x,x] in R ) implies R is reflexive )
proof
assume A1: R is reflexive ; :: thesis: for x being Element of L holds [x,x] in R
let x be Element of L; :: thesis: [x,x] in R
A2: R is_reflexive_in field R by A1, RELAT_2:def 9;
dom R = the carrier of L by PARTFUN1:def 2;
then x in (dom R) \/ (rng R) by XBOOLE_0:def 3;
hence [x,x] in R by A2, RELAT_2:def 1; :: thesis: verum
end;
assume B1: for x being Element of L holds [x,x] in R ; :: thesis: R is reflexive
for x being object st x in field R holds
[x,x] in R
proof
let x be object ; :: thesis: ( x in field R implies [x,x] in R )
b2: field R c= the carrier of L \/ the carrier of L by RELSET_1:8;
assume x in field R ; :: thesis: [x,x] in R
hence [x,x] in R by B1, b2; :: thesis: verum
end;
hence R is reflexive by RELAT_2:def 9, RELAT_2:def 1; :: thesis: verum