now :: thesis: for x being object st x in Y holds
x in dom (T |_2 Y)
let x be object ; :: 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 Th7, ZFMISC_1:87;
then [x,x] in T |_2 Y by XBOOLE_0:def 4;
hence x in dom (T |_2 Y) by XTUPLE_0:def 12; :: thesis: verum
end;
then Y c= dom (T |_2 Y) ;
then dom (T |_2 Y) = Y by XBOOLE_0:def 10;
hence T |_2 Y is Tolerance of Y by Th10, PARTFUN1:def 2, WELLORD1:15; :: thesis: verum