let it1, it2 be set ; ( ( 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]
; it1 = it2
hence
it1 = it2
by TARSKI:2; verum