consider it0 being set such that

A1: for R being set holds

( R in it0 iff ( R in LinPreorders A & S_{1}[R] ) )
from XFAMILY:sch 1();

for R being object st R in it0 holds

R in LinPreorders A by A1;

then reconsider it0 = it0 as Subset of (LinPreorders A) by TARSKI:def 3;

take it0 ; :: thesis: for R being Element of LinPreorders A holds

( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b )

let R be Element of LinPreorders A; :: thesis: ( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b )

thus ( R in it0 implies S_{1}[R] )
by A1; :: thesis: ( ( for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b ) implies R in it0 )

assume S_{1}[R]
; :: thesis: R in it0

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

A1: for R being set holds

( R in it0 iff ( R in LinPreorders A & S

for R being object st R in it0 holds

R in LinPreorders A by A1;

then reconsider it0 = it0 as Subset of (LinPreorders A) by TARSKI:def 3;

take it0 ; :: thesis: for R being Element of LinPreorders A holds

( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b )

let R be Element of LinPreorders A; :: thesis: ( R in it0 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds

a = b )

thus ( R in it0 implies S

a = b ) implies R in it0 )

assume S

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