consider it0 being set such that

A1: for R being set holds

( R in it0 iff ( R in bool [:A,A:] & S_{1}[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_{1}[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_{1}[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

A1: for R being set holds

( R in it0 iff ( R in bool [:A,A:] & S

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

( [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

[:A,A:] in bool [:A,A:] by ZFMISC_1:def 1;

hence R in it0 by A1, A2; :: thesis: verum