let A be non empty Poset; :: thesis: for S being Subset of A holds field (the InternalRel of A |_2 S) = S
let S be Subset of A; :: thesis: field (the InternalRel of A |_2 S) = S
set P = the InternalRel of A |_2 S;
thus field (the InternalRel of A |_2 S) c= S by WELLORD1:20; :: according to XBOOLE_0:def 10 :: thesis: S c= field (the InternalRel of A |_2 S)
thus S c= field (the InternalRel of A |_2 S) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in field (the InternalRel of A |_2 S) )
assume A1: x in S ; :: thesis: x in field (the InternalRel of A |_2 S)
( S c= the carrier of A & the InternalRel of A is_reflexive_in the carrier of A ) by Def4;
then ( [x,x] in the InternalRel of A & [x,x] in [:S,S:] ) by A1, RELAT_2:def 1, ZFMISC_1:106;
then [x,x] in the InternalRel of A |_2 S by XBOOLE_0:def 4;
then ( x in dom (the InternalRel of A |_2 S) & x in rng (the InternalRel of A |_2 S) ) by RELAT_1:def 4, RELAT_1:def 5;
hence x in field (the InternalRel of A |_2 S) by XBOOLE_0:def 3; :: thesis: verum

end;