consider it0 being set such that
A1:
for R being set holds
( R in it0 iff ( R in bool [:A,A:] & S1[R] ) )
from XFAMILY:sch 1();
take
it0
; for R being set holds
( R in it0 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 ) ) )
let R be set ; ( R in it0 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 ) ) )
thus
( R in it0 implies S1[R] )
by A1; ( 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 R in it0 )
assume A2:
S1[R]
; R in it0
[:A,A:] in bool [:A,A:]
by ZFMISC_1:def 1;
hence
R in it0
by A1, A2; verum