let L be complete LATTICE; :: thesis: for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)

let S be non empty full infs-inheriting SubRelStr of L; :: thesis: Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)

the carrier of (Image (closure_op S)) = the carrier of S

let S be non empty full infs-inheriting SubRelStr of L; :: thesis: Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)

the carrier of (Image (closure_op S)) = the carrier of S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S or x in the carrier of (Image (closure_op S)) )

assume x in the carrier of S ; :: thesis: x in the carrier of (Image (closure_op S))

then reconsider a = x as Element of S ;

reconsider a = a as Element of L by YELLOW_0:58;

set X = (uparrow a) /\ the carrier of S;

A3: (id L) . a = a ;

a <= a ;

then a in uparrow a by WAYBEL_0:18;

then A4: a in (uparrow a) /\ the carrier of S by XBOOLE_0:def 4;

(closure_op S) . a = "/\" (((uparrow a) /\ the carrier of S),L) by Def5;

then A5: (closure_op S) . a <= a by A4, YELLOW_2:22;

id L <= closure_op S by WAYBEL_1:def 14;

then a <= (closure_op S) . a by A3, YELLOW_2:9;

then A6: a = (closure_op S) . a by A5, ORDERS_2:2;

dom (closure_op S) = the carrier of L by FUNCT_2:def 1;

then a in rng (closure_op S) by A6, FUNCT_1:def 3;

hence x in the carrier of (Image (closure_op S)) by YELLOW_0:def 15; :: thesis: verum

end;

hence
Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_0:57; :: thesis: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of S c= the carrier of (Image (closure_op S))

set c = closure_op S;let x be object ; :: thesis: ( x in the carrier of (Image (closure_op S)) implies x in the carrier of S )

assume x in the carrier of (Image (closure_op S)) ; :: thesis: x in the carrier of S

then reconsider a = x as Element of (Image (closure_op S)) ;

consider b being Element of L such that

A1: a = (closure_op S) . b by YELLOW_2:10;

set X = (uparrow b) /\ the carrier of S;

reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17;

A2: ex_inf_of X,L by YELLOW_0:17;

a = "/\" (X,L) by A1, Def5;

hence x in the carrier of S by A2, YELLOW_0:def 18; :: thesis: verum

end;assume x in the carrier of (Image (closure_op S)) ; :: thesis: x in the carrier of S

then reconsider a = x as Element of (Image (closure_op S)) ;

consider b being Element of L such that

A1: a = (closure_op S) . b by YELLOW_2:10;

set X = (uparrow b) /\ the carrier of S;

reconsider X = (uparrow b) /\ the carrier of S as Subset of S by XBOOLE_1:17;

A2: ex_inf_of X,L by YELLOW_0:17;

a = "/\" (X,L) by A1, Def5;

hence x in the carrier of S by A2, YELLOW_0:def 18; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S or x in the carrier of (Image (closure_op S)) )

assume x in the carrier of S ; :: thesis: x in the carrier of (Image (closure_op S))

then reconsider a = x as Element of S ;

reconsider a = a as Element of L by YELLOW_0:58;

set X = (uparrow a) /\ the carrier of S;

A3: (id L) . a = a ;

a <= a ;

then a in uparrow a by WAYBEL_0:18;

then A4: a in (uparrow a) /\ the carrier of S by XBOOLE_0:def 4;

(closure_op S) . a = "/\" (((uparrow a) /\ the carrier of S),L) by Def5;

then A5: (closure_op S) . a <= a by A4, YELLOW_2:22;

id L <= closure_op S by WAYBEL_1:def 14;

then a <= (closure_op S) . a by A3, YELLOW_2:9;

then A6: a = (closure_op S) . a by A5, ORDERS_2:2;

dom (closure_op S) = the carrier of L by FUNCT_2:def 1;

then a in rng (closure_op S) by A6, FUNCT_1:def 3;

hence x in the carrier of (Image (closure_op S)) by YELLOW_0:def 15; :: thesis: verum