let it1, it2 be Subset of (LinPreorders A); :: thesis: ( ( for R being Element of LinPreorders A holds
( R in it1 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) & ( for R being Element of LinPreorders A holds
( R in it2 iff for a, b being Element of A st [a,b] in R & [b,a] in R holds
a = b ) ) implies it1 = it2 )
assume that
A4: S₂[it1] and
A5: S₂[it2] ; :: thesis: it1 = it2

now

let R be Element of LinPreorders A; :: thesis: ( R in it1 iff R in it2 )
( R in it1 iff S₁[R] ) by A4;
hence ( R in it1 iff R in it2 ) by A5; :: thesis: verum

end;

hence it1 = it2 by SUBSET_1:8; :: thesis: verum