defpred S_{1}[ 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_{1}[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 ) )

M c= Y ) )

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

( $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

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

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 x in M

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

assume A3: x in X ; :: thesis: x in M

end;assume A3: x in X ; :: thesis: x in M

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

x in Y

hence
x in M
by A2, SETFAM_1:def 1; :: thesis: verumx 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;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

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

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

end;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

hence
f .: M c= M
; :: thesis: verumy 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

end;assume A6: y in f .: M ; :: thesis: y in M

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

y in Y

hence
y in M
by A2, SETFAM_1:def 1; :: thesis: verumy 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;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

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