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

A1: now :: thesis: for x being Element of L holds
( (id L) . x = x & (id L) . x <= (closure_op S) . x )

let x be Element of L; :: thesis: ( (id L) . x = x & (id L) . x <= (closure_op S) . x )
thus (id L) . x = x ; :: thesis: (id L) . x <= (closure_op S) . x
(uparrow x) /\ the carrier of S c= uparrow x by XBOOLE_1:17;
then A2: 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 Def5;
hence (id L) . x <= (closure_op S) . x by A2, YELLOW_0:33; :: thesis: verum

end;

now :: thesis: for x being Element of L holds cc . x = (closure_op S) . x

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;
A3: (closure_op S) . ((closure_op S) . x) = "/\" (((uparrow ((closure_op S) . x)) /\ the carrier of S),L) by Def5;
(closure_op S) . x <= (closure_op S) . x ;
then A4: (closure_op S) . x in uparrow ((closure_op S) . x) by WAYBEL_0:18;
ex_inf_of X,L by YELLOW_0:17;
then A5: "/\" (X,L) in the carrier of S by YELLOW_0:def 18;
(closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5;
then (closure_op S) . x in (uparrow ((closure_op S) . x)) /\ the carrier of S by A5, A4, XBOOLE_0:def 4;
then A6: (closure_op S) . ((closure_op S) . x) <= (closure_op S) . x by A3, YELLOW_2:22;
A7: (closure_op S) . ((closure_op S) . x) >= (id L) . ((closure_op S) . x) by A1;
thus cc . x = (closure_op S) . ((closure_op S) . x) by FUNCT_2:15
.= (closure_op S) . x by A6, A7, ORDERS_2:2 ; :: thesis: verum

end;

hence (closure_op S) * (closure_op S) = closure_op S by FUNCT_2:63; :: 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 )
A8: ex_inf_of (uparrow x) /\ the carrier of S,L by YELLOW_0:17;
A9: 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 A10: (uparrow y) /\ the carrier of S c= (uparrow x) /\ the carrier of S by WAYBEL_0:22, XBOOLE_1:26;
A11: (closure_op S) . y = "/\" (((uparrow y) /\ the carrier of S),L) by Def5;
(closure_op S) . x = "/\" (((uparrow x) /\ the carrier of S),L) by Def5;
hence (closure_op S) . x <= (closure_op S) . y by A10, A8, A9, A11, 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