defpred S1[ 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 & S1[Y] ) ) from 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 ; :: 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 ;
then f .: M c= Y by A8;
hence y in Y by A6; :: thesis: verum
end;
hence y in M by ; :: 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 ;
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