set c = closure_op S;
reconsider cc = (closure_op S) * (closure_op S) as Function of L,L ;

A1: now

let x be Element of L; :: thesis: ( (id L) . x = x & (id L) . x <= (closure_op S) . x )
thus A2: (id L) . x = x by TMAP_1:91; :: thesis: (id L) . x <= (closure_op S) . x
A3: (closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L by Def6;
( x is_<=_than uparrow x & (uparrow x) /\ the carrier of S c= uparrow x ) by XBOOLE_1:17, YELLOW_2:2;
then x is_<=_than (uparrow x) /\ the carrier of S by YELLOW_0:9;
hence (id L) . x <= (closure_op S) . x by A2, A3, YELLOW_0:33; :: thesis: verum

end;

now

let x be Element of L; :: thesis: cc . x = (closure_op S) . x
set y = (closure_op S) . x;
A4: (closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L by Def6;
A5: (closure_op S) . ((closure_op S) . x) = "/\" ((uparrow ((closure_op S) . x)) /\ the carrier of S),L by Def6;
set X = (uparrow x) /\ the carrier of S;
reconsider X = (uparrow x) /\ the carrier of S as Subset of S by XBOOLE_1:17;
A6: ( (closure_op S) . x <= (closure_op S) . x & ex_inf_of X,L ) by YELLOW_0:17;
then "/\" X,L in the carrier of S by YELLOW_0:def 18;
then ( (closure_op S) . x in uparrow ((closure_op S) . x) & (closure_op S) . x = inf X & inf X in the carrier of S ) by A4, A6, WAYBEL_0:18, YELLOW_0:64;
then (closure_op S) . x in (uparrow ((closure_op S) . x)) /\ the carrier of S by XBOOLE_0:def 4;
then A7: (closure_op S) . ((closure_op S) . x) <= (closure_op S) . x by A5, YELLOW_2:24;
A8: ( (closure_op S) . ((closure_op S) . x) >= (id L) . ((closure_op S) . x) & (id L) . ((closure_op S) . x) = (closure_op S) . x ) by A1;
thus cc . x = (closure_op S) . ((closure_op S) . x) by FUNCT_2:21
.= (closure_op S) . x by A7, A8, ORDERS_2:25 ; :: thesis: verum

end;

hence (closure_op S) * (closure_op S) = closure_op S by FUNCT_2:113; :: according to QUANTAL1:def 9,WAYBEL_1:def 13,WAYBEL_1:def 14 :: thesis: ( closure_op S is monotone & id L <= closure_op S )

hereby :: according to WAYBEL_1:def 2 :: thesis: id L <= closure_op S

let x, y be Element of L; :: thesis: ( x <= y implies (closure_op S) . x <= (closure_op S) . y )
assume x <= y ; :: thesis: (closure_op S) . x <= (closure_op S) . y
then uparrow y c= uparrow x by WAYBEL_0:22;
then ( (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S & ex_inf_of (uparrow x) /\ the carrier of S,L & ex_inf_of (uparrow y) /\ the carrier of S,L & (closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L & (closure_op S) . y = "/\" ((uparrow y) /\ the carrier of S),L ) by Def6, XBOOLE_1:26, YELLOW_0:17;
hence (closure_op S) . x <= (closure_op S) . y by YELLOW_0:35; :: thesis: verum

end;

let x be set ; :: according to YELLOW_2:def 1 :: thesis: ( not x in the carrier of L or ex b₁, b₂ being Element of the carrier of L st
( b₁ = (id L) . x & b₂ = (closure_op S) . x & b₁ <= b₂ ) )
assume x in the carrier of L ; :: thesis: ex b₁, b₂ being Element of the carrier of L st
( b₁ = (id L) . x & b₂ = (closure_op S) . x & b₁ <= b₂ )
then reconsider x = x as Element of L ;
(id L) . x <= (closure_op S) . x by A1;
hence ex b₁, b₂ being Element of the carrier of L st
( b₁ = (id L) . x & b₂ = (closure_op S) . x & b₁ <= b₂ ) ; :: thesis: verum