let L be complete LATTICE; :: thesis: Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp

defpred S_{1}[ object ] means $1 is strict closure directed-sups-inheriting System of L;

( a is Element of ((Subalgebras L) opp) iff S_{1}[a] )
by Th27;

RelStr(# the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the InternalRel of (Image ((ClImageMap L) | (DsupClOpers L))) #) = RelStr(# the carrier of ((Subalgebras L) opp), the InternalRel of ((Subalgebras L) opp) #) from WAYBEL10:sch 3(A1, A3);

hence Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp ; :: thesis: verum

defpred S

A1: now :: thesis: for a being object holds

( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S_{1}[a] ) & ( S_{1}[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) )

A3:
for a being object holds ( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S

let a be object ; :: thesis: ( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S_{1}[a] ) & ( S_{1}[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) )

_{1}[a]
; :: thesis: a is Element of (Image ((ClImageMap L) | (DsupClOpers L)))

then reconsider S = a as strict closure directed-sups-inheriting System of L ;

reconsider x = closure_op S as Element of (DsupClOpers L) by Th26;

S = Image (closure_op S) by Th18

.= (ClImageMap L) . (closure_op S) by Def4

.= ((ClImageMap L) | (DsupClOpers L)) . x by Th6 ;

then S in rng ((ClImageMap L) | (DsupClOpers L)) by FUNCT_2:4;

hence a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) by YELLOW_0:def 15; :: thesis: verum

end;hereby :: thesis: ( S_{1}[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) )

assume
Sassume
a is Element of (Image ((ClImageMap L) | (DsupClOpers L)))
; :: thesis: S_{1}[a]

then consider x being Element of (DsupClOpers L) such that

A2: ((ClImageMap L) | (DsupClOpers L)) . x = a by YELLOW_2:10;

reconsider x = x as directed-sups-preserving closure Function of L,L by Th26;

a = (ClImageMap L) . x by A2, Th6

.= Image x by Def4 ;

hence S_{1}[a]
; :: thesis: verum

end;then consider x being Element of (DsupClOpers L) such that

A2: ((ClImageMap L) | (DsupClOpers L)) . x = a by YELLOW_2:10;

reconsider x = x as directed-sups-preserving closure Function of L,L by Th26;

a = (ClImageMap L) . x by A2, Th6

.= Image x by Def4 ;

hence S

then reconsider S = a as strict closure directed-sups-inheriting System of L ;

reconsider x = closure_op S as Element of (DsupClOpers L) by Th26;

S = Image (closure_op S) by Th18

.= (ClImageMap L) . (closure_op S) by Def4

.= ((ClImageMap L) | (DsupClOpers L)) . x by Th6 ;

then S in rng ((ClImageMap L) | (DsupClOpers L)) by FUNCT_2:4;

hence a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) by YELLOW_0:def 15; :: thesis: verum

( a is Element of ((Subalgebras L) opp) iff S

RelStr(# the carrier of (Image ((ClImageMap L) | (DsupClOpers L))), the InternalRel of (Image ((ClImageMap L) | (DsupClOpers L))) #) = RelStr(# the carrier of ((Subalgebras L) opp), the InternalRel of ((Subalgebras L) opp) #) from WAYBEL10:sch 3(A1, A3);

hence Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp ; :: thesis: verum