reconsider b = RelStr(# a,r #) as object of by A1, Def10;
b = latt b ;
then A2: ex b being object of st S₁[b] ;
thus ex C being non empty strict full subcategory of non empty strict semi-functional full para-functional set-id-inheriting concrete carrier-underlaid lattice-wise with_complete_lattices with_all_isomorphisms st
for a being object of holds
( a is object of iff S₁[a] ) from YELLOW20:sch 2(A2); :: thesis: verum