thus W -INF_category is lattice-wise ; :: according to YELLOW21:def 5 :: thesis: for b₁ being Element of the carrier of (W -INF_category) holds b₁ is RelStr
let a be Object of (W -INF_category); :: thesis: a is RelStr
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
a = latt a ;
hence a is RelStr by A1, Def4; :: thesis: verum