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

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