now

let x be set ; :: thesis: ( x in Y implies x in dom (T |_2 Y) )
assume x in Y ; :: thesis: x in dom (T |_2 Y)
then ( [x,x] in [:Y,Y:] & [x,x] in T ) by Th27, ZFMISC_1:87;
then [x,x] in T |_2 Y by 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 2, WELLORD1:15; :: thesis: verum