consider it0 being set such that
A1: for R being set holds
( R in it0 iff ( R in LinPreorders A & S₁[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₁[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₁[R] ; :: thesis: R in it0
hence R in it0 by A1; :: thesis: verum