let A, B be set ; :: thesis: ( ( for x being object holds

( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being object holds

( x in B iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) implies A = B )

assume that

A1: for x being object holds

( x in A iff S_{1}[x] )
and

A2: for x being object holds

( x in B iff S_{1}[x] )
; :: thesis: A = B

thus A = B from XBOOLE_0:sch 2(A1, A2); :: thesis: verum

( x in A iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) & ( for x being object holds

( x in B iff ( x is strict Poset & the carrier of (x as_1-sorted) in W ) ) ) implies A = B )

assume that

A1: for x being object holds

( x in A iff S

A2: for x being object holds

( x in B iff S

thus A = B from XBOOLE_0:sch 2(A1, A2); :: thesis: verum