let D1, D2 be Subset of LTLB_WFF; :: thesis: ( D1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D2 c= D ) implies D1 = D2 )

assume ( D1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D2 c= D ) ) ; :: thesis: D1 = D2

then ( D1 c= D2 & D2 c= D1 ) ;

hence D1 = D2 by XBOOLE_0:def 10; :: thesis: verum

D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D2 c= D ) implies D1 = D2 )

assume ( D1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D2 c= D ) ) ; :: thesis: D1 = D2

then ( D1 c= D2 & D2 c= D1 ) ;

hence D1 = D2 by XBOOLE_0:def 10; :: thesis: verum