set KC = { (conv (@ A)) where A is Subset of Kr : A is simplex-like } ;
{ (conv (@ A)) where A is Subset of Kr : A is simplex-like } c= bool the carrier of RLS

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (conv (@ A)) where A is Subset of Kr : A is simplex-like } ; :: thesis:
then ex A being Subset of Kr st
( x = conv (@ A) & A is simplex-like ) ;
hence x in bool the carrier of RLS ; :: thesis:

end;

then reconsider KC = { (conv (@ A)) where A is Subset of Kr : A is simplex-like } as Subset-Family of RLS ;
take IT = union KC; :: thesis:
let x be set ; :: thesis:

hereby :: thesis:

assume x in IT ; :: thesis:
then consider y being set such that
A1: x in y and
A2: y in KC by TARSKI:def 4;
consider A being Subset of Kr such that
A3: ( y = conv (@ A) & A is simplex-like ) by A2;
take A = A; :: thesis:
thus ( A is simplex-like & x in conv (@ A) ) by A1, A3; :: thesis:

end;

given A being Subset of Kr such that A4: A is simplex-like and
A5: x in conv (@ A) ; :: thesis:
conv (@ A) in KC by A4;
hence x in IT by A5, TARSKI:def 4; :: thesis: