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

( 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

A c= B
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;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

proof

hence
A = B
by A4, XBOOLE_0:def 10; :: thesis: verum
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;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