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