defpred S1[ object ] means ex y, z being object st
( $1 = [y,z] & P1[y,z] );
consider T being set such that
A3: for x being object holds
( x in T iff ( x in [:F1(),F1():] & S1[x] ) ) from XBOOLE_0:sch 1();
 for x being object st x in T holds
x in [:F1(),F1():] by A3;
then reconsider T = T as Relation of F1(),F1() by TARSKI:def 3;
A4: field T c= F1() \/ F1() by RELSET_1:8;
for x being object st x in field T holds
[x,x] in T
proof
let x be object ; :: thesis: ( x in field T implies [x,x] in T )
assume x in field T ; :: thesis: [x,x] in T
then ( [x,x] in [:F1(),F1():] & P1[x,x] ) by A1, A4, ZFMISC_1:87;
hence [x,x] in T by A3; :: thesis: verum
end;
then A5: T is_reflexive_in field T ;
for x, y being object st x in field T & y in field T & [x,y] in T holds
[y,x] in T
proof
let x, y be object ; :: thesis: ( x in field T & y in field T & [x,y] in T implies [y,x] in T )
assume that
A6: ( x in field T & y in field T ) and
A7: [x,y] in T ; :: thesis: [y,x] in T
( x in F1() & y in F1() & P1[x,y] )
proof
thus ( x in F1() & y in F1() ) by A4, A6; :: thesis: P1[x,y]
consider a, b being object such that
A8: [x,y] = [a,b] and
A9: P1[a,b] by A3, A7;
x = a by A8, XTUPLE_0:1;
hence P1[x,y] by A8, A9, XTUPLE_0:1; :: thesis: verum
end;
then ( [y,x] in [:F1(),F1():] & P1[y,x] ) by A2, ZFMISC_1:87;
hence [y,x] in T by A3; :: thesis: verum
end;
then A10: T is_symmetric_in field T ;
for x being object st x in F1() holds
x in dom T
proof
let x be object ; :: thesis: ( x in F1() implies x in dom T )
assume x in F1() ; :: thesis: x in dom T
then ( [x,x] in [:F1(),F1():] & P1[x,x] ) by A1, ZFMISC_1:87;
then [x,x] in T by A3;
hence x in dom T by XTUPLE_0:def 12; :: thesis: verum
end;
then F1() c= dom T ;
then dom T = F1() by XBOOLE_0:def 10;
then reconsider T = T as Tolerance of F1() by A5, A10, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 11;
take T ; :: thesis: for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
let x, y be set ; :: thesis: ( x in F1() & y in F1() implies ( [x,y] in T iff P1[x,y] ) )
assume A11: ( x in F1() & y in F1() ) ; :: thesis: ( [x,y] in T iff P1[x,y] )
thus ( [x,y] in T implies P1[x,y] ) :: thesis: ( P1[x,y] implies [x,y] in T )
proof
assume [x,y] in T ; :: thesis: P1[x,y]
then consider a, b being object such that
A12: [x,y] = [a,b] and
A13: P1[a,b] by A3;
x = a by A12, XTUPLE_0:1;
hence P1[x,y] by A12, A13, XTUPLE_0:1; :: thesis: verum
end;
assume A14: P1[x,y] ; :: thesis: [x,y] in T
[x,y] in [:F1(),F1():] by A11, ZFMISC_1:87;
hence [x,y] in T by A3, A14; :: thesis: verum