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: S_{2}[it1]
and

A4: S_{2}[it2]
; :: thesis: it1 = it2

( 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: S

A4: S

now :: thesis: for R being object holds

( R in it1 iff R in it2 )

hence
it1 = it2
by TARSKI:2; :: thesis: verum( 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 S_{1}[RR] )
by A3;

hence ( R in it1 iff R in it2 ) by A4; :: thesis: verum

end;reconsider RR = R as set by TARSKI:1;

( R in it1 iff S

hence ( R in it1 iff R in it2 ) by A4; :: thesis: verum