let a be set ; :: according to ORDERS_3:def 4 :: thesis: ( not a in POSETS W or a is RelStr )
assume A1: a in POSETS W ; :: thesis: a is RelStr
then A2: ( a is strict Poset & the carrier of (a as_1-sorted ) in W ) by Def2;
reconsider a = a as Poset by A1, Def2;
( a = a as_1-sorted & the carrier of (a as_1-sorted ) <> {} ) by A2, Def1;
hence a is RelStr ; :: thesis: verum