now

let x be set ; :: thesis: ( x in Y implies x in dom (T |_2 Y) )
assume A1: x in Y ; :: thesis: x in dom (T |_2 Y)
then A2: [x,x] in [:Y,Y:] by ZFMISC_1:106;
[x,x] in T by A1, Th27;
then [x,x] in T |_2 Y by A2, XBOOLE_0:def 4;
hence x in dom (T |_2 Y) by RELAT_1:def 4; :: thesis: verum

end;

then Y c= dom (T |_2 Y) by TARSKI:def 3;
then dom (T |_2 Y) = Y by XBOOLE_0:def 10;
hence T |_2 Y is Tolerance of Y by Th32, PARTFUN1:def 4, WELLORD1:22; :: thesis: verum