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
A4: S₂[it1] and
A5: 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 A4;
hence ( R in it1 iff R in it2 ) by A5; :: thesis: verum

end;

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