let Y, Z be Subset of LTLB_WFF; :: thesis: ( ( for x being set holds

( x in Y iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) & ( for x being set holds

( x in Z iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) implies Y = Z )

assume that

A7: for x being set holds

( x in Y iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) and

A8: for x being set holds

( x in Z iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ; :: thesis: Y = Z

thus Y c= Z :: according to XBOOLE_0:def 10 :: thesis: Z c= Y

( x in Y iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) & ( for x being set holds

( x in Z iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ) implies Y = Z )

assume that

A7: for x being set holds

( x in Y iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) and

A8: for x being set holds

( x in Z iff ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) ) ; :: thesis: Y = Z

thus Y c= Z :: according to XBOOLE_0:def 10 :: thesis: Z c= Y

proof

thus
Z c= Y
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Z )

assume x in Y ; :: thesis: x in Z

then ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) by A7;

hence x in Z by A8; :: thesis: verum

end;assume x in Y ; :: thesis: x in Z

then ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) by A7;

hence x in Z by A8; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in Y )

assume x in Z ; :: thesis: x in Y

then ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) by A8;

hence x in Y by A7; :: thesis: verum

end;assume x in Z ; :: thesis: x in Y

then ex A being Element of LTLB_WFF st

( A in X & x in tau1 . A ) by A8;

hence x in Y by A7; :: thesis: verum