let X be set ; :: thesis: for R being Relation of X st X c= field R holds
R [*] is_reflexive_in X
let R be Relation of X; :: thesis: ( X c= field R implies R [*] is_reflexive_in X )
assume A1: X c= field R ; :: thesis: R [*] is_reflexive_in X
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R [*] )
assume A2: x in X ; :: thesis: [x,x] in R [*]
set p = <*x*>;
A3: len <*x*> = 1 by FINSEQ_1:40;
then A4: <*x*> . (len <*x*>) = x ;
for i being Nat st i >= 1 & i < len <*x*> holds
[(<*x*> . i),(<*x*> . (i + 1))] in R by FINSEQ_1:40;
hence [x,x] in R [*] by A1, A2, A3, A4, FINSEQ_1:def 17; :: thesis: verum