let a, b be Element of L; :: thesis:
set X = { x where x is Element of L : ( x >= a & x >= b ) } ;
{ x where x is Element of L : ( x >= a & x >= b ) } c= the carrier of L

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { x where x is Element of L : ( x >= a & x >= b ) } ; :: thesis:
then ex z being Element of L st
( x = z & z >= a & z >= b ) ;
hence x in the carrier of L ; :: thesis:

end;

then reconsider X = { x where x is Element of L : ( x >= a & x >= b ) } as Subset of L ;
A2: Top L >= a by YELLOW_0:45;
Top L >= b by YELLOW_0:45;
then Top L in X by A2;
then ex_inf_of X,L by A1, Th76;
then consider c being Element of L such that
A3: c is_<=_than X and
A4: for d being Element of L st d is_<=_than X holds
d <= c and
for e being Element of L st e is_<=_than X & ( for d being Element of L st d is_<=_than X holds
d <= e ) holds
e = c ;
A5: c is_>=_than {a,b}

let y be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume y in X ; :: thesis:
then ex z being Element of L st
( y = z & z >= a & z >= b ) ;
hence x <= y by A6, TARSKI:def 2; :: thesis:

end;

hence x <= c by A4; :: thesis:

end;

end;

end;