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

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 X' being Subset of L st
( X' = X & F c= X' & X' is Ideal of L ) ;
hence F c= X ; :: thesis: verum

end;

then A4: F c= meet { I where I is Subset of L : ( F c= I & I is Ideal of L ) } by A2, SETFAM_1:6;
consider x being set such that
A5: x in F by A1, XBOOLE_0:def 1;
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 A2, A4, A5, SETFAM_1:4;
A6: 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 A7: ( x in I & y in I ) ; :: thesis: x + y in I

now

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 A8: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(x + y)} c= X
then A9: x in X by A7, SETFAM_1:def 1;
A10: y in X by A7, A8, SETFAM_1:def 1;
consider X' being Subset of L such that
A11: ( X' = X & F c= X' & X' is Ideal of L ) by A8;
x + y in X' by A9, A10, A11, Def1;
hence {(x + y)} c= X by A11, ZFMISC_1:37; :: thesis: verum

end;

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

end;

A12: 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 A13: x in I ; :: thesis: p * x in I

now

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 A14: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(p * x)} c= X
then A15: x in X by A13, SETFAM_1:def 1;
consider X' being Subset of L such that
A16: ( X' = X & F c= X' & X' is Ideal of L ) by A14;
p * x in X' by A15, A16, Def2;
hence {(p * x)} c= X by A16, ZFMISC_1:37; :: thesis: verum

end;

then {(p * x)} c= I by A2, SETFAM_1:6;
hence p * x in I by ZFMISC_1:37; :: 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 A17: x in I ; :: thesis: x * p in I

now

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 A18: X in { I where I is Subset of L : ( F c= I & I is Ideal of L ) } ; :: thesis: {(x * p)} c= X
then A19: x in X by A17, SETFAM_1:def 1;
consider X' being Subset of L such that
A20: ( X' = X & F c= X' & X' is Ideal of L ) by A18;
x * p in X' by A19, A20, Def3;
hence {(x * p)} c= X by A20, ZFMISC_1:37; :: thesis: verum

end;

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

end;

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

now

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:4; :: 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:6; :: thesis: verum