let S1, S2 be Subset of RLS; :: thesis: ( ( for x being set holds
( x in S1 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) ) & ( for x being set holds
( x in S2 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) ) implies S1 = S2 )
assume that
A6: for x being set holds
( x in S1 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) and
A7: for x being set holds
( x in S2 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) ; :: thesis: S1 = S2

now :: thesis: for x being object holds
( x in S1 iff x in S2 )

let x be object ; :: thesis: ( x in S1 iff x in S2 )
( x in S1 iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) by A6;
hence ( x in S1 iff x in S2 ) by A7; :: thesis: verum

end;

hence S1 = S2 by TARSKI:2; :: thesis: verum