consider it0 being set such that
A1: for R being set holds
( R in it0 iff ( R in LinPreorders A & S₁[R] ) ) from XBOOLE_0:sch 1();
A2: for R being set st R in it0 holds
R in LinPreorders A by A1;
reconsider it0 = it0 as Subset of (LinPreorders A) by A2, 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 A3: S₁[R] ; :: thesis: R in it0
thus R in it0 by A1, A3; :: thesis: verum