defpred S₁[ set ] means ex B being Subset of E st
( $1 = B & X c= $1 & B is_stable_under_the_action_of A );
consider XX being set such that
A1: for Y being set holds
( Y in XX iff ( Y in bool E & S₁[Y] ) ) from XFAMILY:sch 1();
set M = meet XX;
[#] E is_stable_under_the_action_of A ;
then A2: E in XX by A1;
then for x being object st x in meet XX holds
x in E by SETFAM_1:def 1;
then reconsider M = meet XX as Subset of E by TARSKI:def 3;
take M ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A3: x in X ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in XX ; :: thesis:
then ex B being Subset of E st
( Y = B & X c= Y & B is_stable_under_the_action_of A ) by A1;
hence x in Y by A3; :: thesis:

end;

hence x in M by A2, SETFAM_1:def 1; :: thesis:

end;

hence X c= M ; :: thesis:

now :: thesis:

let o be Element of O; :: thesis:
let f be Function of E,E; :: thesis:
assume A4: o in O ; :: thesis:
assume A5: f = A . o ; :: thesis:

now :: thesis:

let y be object ; :: thesis:
assume A6: y in f .: M ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume A7: Y in XX ; :: thesis:
then ex B being Subset of E st
( Y = B & X c= Y & B is_stable_under_the_action_of A ) by A1;
then A8: f .: Y c= Y by A4, A5;
f .: M c= f .: Y by A7, RELAT_1:123, SETFAM_1:3;
then f .: M c= Y by A8;
hence y in Y by A6; :: thesis:

end;

hence y in M by A2, SETFAM_1:def 1; :: thesis:

end;

hence f .: M c= M ; :: thesis:

end;

hence M is_stable_under_the_action_of A ; :: thesis:
for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
M c= Y by A1, SETFAM_1:3;
hence for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
M c= Y ; :: thesis: