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

A30: now :: thesis: for X being set st X in { I where I is Subset of L : ( F c= I & I is RightIdeal 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 RightIdeal of L ) } implies F c= X )
assume X in { I where I is Subset of L : ( F c= I & I is RightIdeal of L ) } ; :: thesis: F c= X
then ex X9 being Subset of L st
( X9 = X & F c= X9 & X9 is RightIdeal 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 RightIdeal of L ) } by A29, SETFAM_1:5;
then reconsider I = meet { I where I is Subset of L : ( F c= I & I is RightIdeal of L ) } as non empty Subset of L by A1, A29, SETFAM_1:3;
A31: 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 A32: ( 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 RightIdeal 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 RightIdeal of L ) } implies {(x + y)} c= X )
assume A33: X in { I where I is Subset of L : ( F c= I & I is RightIdeal of L ) } ; :: thesis: {(x + y)} c= X
then consider X9 being Subset of L such that
A34: X9 = X and
F c= X9 and
A35: X9 is RightIdeal of L ;
( x in X & y in X ) by A32, A33, SETFAM_1:def 1;
then x + y in X9 by A34, A35, Def1;
hence {(x + y)} c= X by A34, ZFMISC_1:31; :: thesis: verum

end;

then {(x + y)} c= I by A29, SETFAM_1:5;
hence x + y 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 A36: 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 RightIdeal 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 RightIdeal of L ) } implies {(x * p)} c= X )
assume A37: X in { I where I is Subset of L : ( F c= I & I is RightIdeal of L ) } ; :: thesis: {(x * p)} c= X
then consider X9 being Subset of L such that
A38: X9 = X and
F c= X9 and
A39: X9 is RightIdeal of L ;
x in X by A36, A37, SETFAM_1:def 1;
then x * p in X9 by A38, A39, Def3;
hence {(x * p)} c= X by A38, ZFMISC_1:31; :: thesis: verum

end;

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

end;

then reconsider I = I as RightIdeal of L by A31;
take I ; :: thesis: ( F c= I & ( for I being RightIdeal of L st F c= I holds
I c= I ) )

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

let X be RightIdeal 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 RightIdeal of L ) } ;
hence I c= X by SETFAM_1:3; :: thesis: verum

end;

hence ( F c= I & ( for I being RightIdeal of L st F c= I holds
I c= I ) ) by A29, A30, SETFAM_1:5; :: thesis: verum