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: ( X c= M & M 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
M c= Y ) )

now :: thesis: for x being object st x in X holds
x in M

let x be object ; :: thesis: ( x in X implies x in M )
assume A3: x in X ; :: thesis: x in M

now :: thesis: for Y being set st Y in XX holds
x in Y

let Y be set ; :: thesis: ( Y in XX implies x in Y )
assume Y in XX ; :: thesis: x in Y
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: verum

end;

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

end;

hence X c= M ; :: thesis: ( M 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
M c= Y ) )

now :: thesis: for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: M c= M

let o be Element of O; :: thesis: for f being Function of E,E st o in O & f = A . o holds
f .: M c= M
let f be Function of E,E; :: thesis: ( o in O & f = A . o implies f .: M c= M )
assume A4: o in O ; :: thesis: ( f = A . o implies f .: M c= M )
assume A5: f = A . o ; :: thesis: f .: M c= M

now :: thesis: for y being object st y in f .: M holds
y in M

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

now :: thesis: for Y being set st Y in XX holds
y in Y

let Y be set ; :: thesis: ( Y in XX implies y in Y )
assume A7: Y in XX ; :: thesis: y in Y
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: verum

end;

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

end;

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

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
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: verum