let R be Relation; :: thesis: R [*] is_reflexive_in field R
set RR = R [*] ;
set X = field R;
now :: thesis: for x being object st x in field R holds
[x,x] in R [*]
let x be object ; :: thesis: ( x in field R implies [x,x] in R [*] )
reconsider p = <*x*> as 1 -element FinSequence ;
( len p = 1 & p . 1 = x ) by FINSEQ_1:40;
then A1: ( len p >= 1 & p . 1 = x & p . (len p) = x & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ;
assume x in field R ; :: thesis: [x,x] in R [*]
hence [x,x] in R [*] by A1, FINSEQ_1:def 16; :: thesis: verum
end;
hence R [*] is_reflexive_in field R by RELAT_2:def 1; :: thesis: verum