let X be set ; :: thesis: for R being reflexive total Relation of X
for S being Subset of X holds R |_2 S is reflexive total Relation of S
let R be reflexive total Relation of X; :: thesis: for S being Subset of X holds R |_2 S is reflexive total Relation of S
let S be Subset of X; :: thesis: R |_2 S is reflexive total Relation of S
set Q = R |_2 S;
dom (R |_2 S) = S

proof

thus dom (R |_2 S) c= S ; :: according to XBOOLE_0:def 10 :: thesis: S c= dom (R |_2 S)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in dom (R |_2 S) )
assume A1: x in S ; :: thesis: x in dom (R |_2 S)
then x in X ;
then ( x in field R & R is_reflexive_in field R ) by RELAT_2:def 9, ORDERS_1:12;
then [x,x] in R ;
then [x,x] in R |_2 S by A1, Th4;
hence x in dom (R |_2 S) by XTUPLE_0:def 12; :: thesis: verum

end;

hence R |_2 S is reflexive total Relation of S by PARTFUN1:def 2, WELLORD1:15; :: thesis: verum