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

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

hence
S1 = S2
by TARSKI:2; :: thesis: verum( 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;( 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