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₁[x] ) and
A2: for x being object holds
( x in B iff S₁[x] ) ; :: thesis: A = B
thus A = B from XBOOLE_0:sch 2(A1, A2); :: thesis: verum