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 FUNCT_1:35; :: thesis: (id L) . x <= (closure_op S) . x
(uparrow x) /\ the carrier of S c= uparrow x by XBOOLE_1:17;
then A3: x is_<=_than (uparrow x) /\ the carrier of S by YELLOW_2:2;
(closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L by Def6;
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;
set X = (uparrow x) /\ the carrier of S;
reconsider X = (uparrow x) /\ the carrier of S as Subset of S by XBOOLE_1:17;
A4: (closure_op S) . ((closure_op S) . x) = "/\" ((uparrow ((closure_op S) . x)) /\ the carrier of S),L by Def6;
(closure_op S) . x <= (closure_op S) . x ;
then A5: (closure_op S) . x in uparrow ((closure_op S) . x) by WAYBEL_0:18;
ex_inf_of X,L by YELLOW_0:17;
then A6: "/\" X,L in the carrier of S by YELLOW_0:def 18;
(closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L by Def6;
then (closure_op S) . x in (uparrow ((closure_op S) . x)) /\ the carrier of S by A6, A5, XBOOLE_0:def 4;
then A7: (closure_op S) . ((closure_op S) . x) <= (closure_op S) . x by A4, YELLOW_2:24;
A8: (closure_op S) . ((closure_op S) . x) >= (id L) . ((closure_op S) . x) by A1;
A9: (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, A9, 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 )
A10: ex_inf_of (uparrow x) /\ the carrier of S,L by YELLOW_0:17;
A11: ex_inf_of (uparrow y) /\ the carrier of S,L by YELLOW_0:17;
assume x <= y ; :: thesis: (closure_op S) . x <= (closure_op S) . y
then A12: (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S by WAYBEL_0:22, XBOOLE_1:26;
A13: (closure_op S) . y = "/\" ((uparrow y) /\ the carrier of S),L by Def6;
(closure_op S) . x = "/\" ((uparrow x) /\ the carrier of S),L by Def6;
hence (closure_op S) . x <= (closure_op S) . y by A12, A10, A11, A13, 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