let it1, it2 be set ; :: thesis: ( ( for R being set holds
( R in it1 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) & ( for R being set holds
( R in it2 iff ( R is Relation of A & ( for a, b being Element of A holds
( [a,b] in R or [b,a] in R ) ) & ( for a, b, c being Element of A st [a,b] in R & [b,c] in R holds
[a,c] in R ) ) ) ) implies it1 = it2 )
assume that
A3: S2[it1] and
A4: S2[it2] ; :: thesis: it1 = it2
now :: thesis: for R being object holds
( R in it1 iff R in it2 )
let R be object ; :: thesis: ( R in it1 iff R in it2 )
reconsider RR = R as set by TARSKI:1;
( R in it1 iff S1[RR] ) by A3;
hence ( R in it1 iff R in it2 ) by A4; :: thesis: verum
end;
hence it1 = it2 by TARSKI:2; :: thesis: verum