let B1, B2 be Subset of E; :: thesis: ( X c= B1 & B1 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
B1 c= Y ) & X c= B2 & B2 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
B2 c= Y ) implies B1 = B2 )
assume ( X c= B1 & B1 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
B1 c= Y ) & X c= B2 & B2 is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
B2 c= Y ) ) ; :: thesis: B1 = B2
then ( B1 c= B2 & B2 c= B1 ) ;
hence B1 = B2 by XBOOLE_0:def 10; :: thesis: verum