:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :
for X being real-membered set
for b₂ being strict real RelStr holds
( b₂ = RealPoset X iff the carrier of b₂ = X );