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)
then A2: [x,x] in [:S,S:] by ZFMISC_1:106;
the InternalRel of A is_reflexive_in the carrier of A by Def4;
then [x,x] in the InternalRel of A by A1, RELAT_2:def 1;
then [x,x] in the InternalRel of A |_2 S by A2, XBOOLE_0:def 4;
then x in dom (the InternalRel of A |_2 S) by RELAT_1:def 4;
hence x in field (the InternalRel of A |_2 S) by XBOOLE_0:def 3; :: thesis: verum

end;