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

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) ) )

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

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

proof

then reconsider KC = { (conv (@ A)) where A is Subset of Kr : A is simplex-like } as Subset-Family of RLS ;
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;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

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 )

given A being Subset of Kr such that A4:
A is simplex-like
and ( 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;( 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

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