set c = closure_op S;
reconsider cc = (closure_op S) * (closure_op S) as Function of L,L ;
hence
(closure_op S) * (closure_op S) = closure_op S
by FUNCT_2:63; QUANTAL1:def 9,WAYBEL_1:def 13,WAYBEL_1:def 14 ( closure_op S is monotone & id L <= closure_op S )
hereby WAYBEL_1:def 2 id L <= closure_op S
let x,
y be
Element of
L;
( 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
;
(closure_op S) . x <= (closure_op S) . ythen 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;
verum
end;
let x be set ; YELLOW_2:def 1 ( not x in the carrier of L or ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 ) )
assume
x in the carrier of L
; ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 )
then reconsider x = x as Element of L ;
(id L) . x <= (closure_op S) . x
by A1;
hence
ex b1, b2 being Element of the carrier of L st
( b1 = (id L) . x & b2 = (closure_op S) . x & b1 <= b2 )
; verum