let A, B be Subset of LTLB_WFF; :: thesis: ( ( for x being set holds
( x in A iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds
( x in B iff ex n being Element of NAT st x = prop n ) ) implies A = B )
assume that
A2: for x being set holds
( x in A iff ex n being Element of NAT st x = prop n ) and
A3: for x being set holds
( x in B iff ex n being Element of NAT st x = prop n ) ; :: thesis: A = B
A4: B c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume x in B ; :: thesis: x in A
then consider n being Element of NAT such that
A5: x = prop n by A3;
thus x in A by A2, A5; :: thesis: verum

end;

A c= B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume x in A ; :: thesis: x in B
then consider n being Element of NAT such that
A6: x = prop n by A2;
thus x in B by A3, A6; :: thesis: verum

end;

hence A = B by A4, XBOOLE_0:def 10; :: thesis: verum