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: the carrier of (a as_1-sorted) in W by Def2;
reconsider a = a as Poset by A1, Def2;
a = a as_1-sorted by Def1;
hence a is RelStr by A2; :: thesis: verum