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:13; :: 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 object ; :: 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:87;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then [x,x] in the InternalRel of A by A1;
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 XTUPLE_0:def 12;
hence x in field ( the InternalRel of A |_2 S) by XBOOLE_0:def 3; :: thesis: verum
end;