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

A2: S_{2}[it1]
and

A3: S_{2}[it2]
; :: thesis: it1 = it2

( 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

A2: S

A3: S

now :: thesis: for R being Element of LinPreorders A holds

( R in it1 iff R in it2 )

hence
it1 = it2
by SUBSET_1:3; :: thesis: verum( R in it1 iff R in it2 )

let R be Element of LinPreorders A; :: thesis: ( R in it1 iff R in it2 )

( R in it1 iff S_{1}[R] )
by A2;

hence ( R in it1 iff R in it2 ) by A3; :: thesis: verum

end;( R in it1 iff S

hence ( R in it1 iff R in it2 ) by A3; :: thesis: verum