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: ( not x in { (conv (@ A)) where A is Subset of Kr : A is simplex-like } or x in bool the carrier of RLS )
assume x in { (conv (@ A)) where A is Subset of Kr : A is simplex-like } ; :: thesis: x in bool the carrier of RLS
then ex A being Subset of Kr st
( x = conv (@ A) & A is simplex-like ) ;
hence x in bool the carrier of RLS ; :: thesis: verum

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: for x being set holds
( x in IT iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) )
let x be set ; :: thesis: ( x in IT iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) )

hereby :: thesis: ( ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) implies x in IT )

assume x in IT ; :: thesis: ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) )
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: ( A is simplex-like & x in conv (@ A) )
thus ( A is simplex-like & x in conv (@ A) ) by A1, A3; :: thesis: verum

end;

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