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 A2: ( S₂[it1] & S₂[it2] ) ; :: thesis: it1 = it2

now

let R be set ; :: thesis: ( R in it1 iff R in it2 )
( R in it1 iff S₁[R] ) by A2;
hence ( R in it1 iff R in it2 ) by A2; :: thesis: verum

end;

hence it1 = it2 by TARSKI:2; :: thesis: verum