set Id = { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ;
set I = meet { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ;
the carrier of L is Ideal of L by Th10;
then A2: the carrier of L in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ;

A3: now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } holds
F c= X

let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } implies F c= X )
assume X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: F c= X
then ex X9 being Subset of L st
( X9 = X & F c= X9 & X9 is Ideal of L ) ;
hence F c= X ; :: thesis: verum

end;

then F c= meet { I where I is Subset of L : ( F c= I & I is Ideal of L ) } by A2, SETFAM_1:5;
then reconsider I = meet { I where I is Subset of L : ( F c= I & I is Ideal of L ) } as non empty Subset of L by A1, A2, SETFAM_1:3;
A4: I is add-closed

proof

let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis: ( x in I & y in I implies x + y in I )
assume A5: ( x in I & y in I ) ; :: thesis: x + y in I

now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } holds
{(x + y)} c= X

let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } implies {(x + y)} c= X )
assume A6: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(x + y)} c= X
then consider X9 being Subset of L such that
A7: X9 = X and
F c= X9 and
A8: X9 is Ideal of L ;
( x in X & y in X ) by A5, A6, SETFAM_1:def 1;
then x + y in X9 by A7, A8, Def1;
hence {(x + y)} c= X by A7, ZFMISC_1:31; :: thesis: verum

end;

then {(x + y)} c= I by A2, SETFAM_1:5;
hence x + y in I by ZFMISC_1:31; :: thesis: verum

end;

A9: I is left-ideal

proof

let p, x be Element of L; :: according to IDEAL_1:def 2 :: thesis: ( x in I implies p * x in I )
assume A10: x in I ; :: thesis: p * x in I

now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } holds
{(p * x)} c= X

let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } implies {(p * x)} c= X )
assume A11: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(p * x)} c= X
then consider X9 being Subset of L such that
A12: X9 = X and
F c= X9 and
A13: X9 is Ideal of L ;
x in X by A10, A11, SETFAM_1:def 1;
then p * x in X9 by A12, A13, Def2;
hence {(p * x)} c= X by A12, ZFMISC_1:31; :: thesis: verum

end;

then {(p * x)} c= I by A2, SETFAM_1:5;
hence p * x in I by ZFMISC_1:31; :: thesis: verum

end;

I is right-ideal

proof

let p, x be Element of L; :: according to IDEAL_1:def 3 :: thesis: ( x in I implies x * p in I )
assume A14: x in I ; :: thesis: x * p in I

now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } holds
{(x * p)} c= X

let X be set ; :: thesis: ( X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } implies {(x * p)} c= X )
assume A15: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(x * p)} c= X
then consider X9 being Subset of L such that
A16: X9 = X and
F c= X9 and
A17: X9 is Ideal of L ;
x in X by A14, A15, SETFAM_1:def 1;
then x * p in X9 by A16, A17, Def3;
hence {(x * p)} c= X by A16, ZFMISC_1:31; :: thesis: verum

end;

then {(x * p)} c= I by A2, SETFAM_1:5;
hence x * p in I by ZFMISC_1:31; :: thesis: verum

end;

then reconsider I = I as Ideal of L by A4, A9;
take I ; :: thesis: ( F c= I & ( for I being Ideal of L st F c= I holds
I c= I ) )

now :: thesis: for X being Ideal of L st F c= X holds
I c= X

let X be Ideal of L; :: thesis: ( F c= X implies I c= X )
assume F c= X ; :: thesis: I c= X
then X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ;
hence I c= X by SETFAM_1:3; :: thesis: verum

end;

hence ( F c= I & ( for I being Ideal of L st F c= I holds
I c= I ) ) by A2, A3, SETFAM_1:5; :: thesis: verum