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

proof

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;

thus Z c= Y :: 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;