let L be complete LATTICE; :: thesis: Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp
defpred S1[ object ] means $1 is strict closure directed-sups-inheriting System of L;
A1: now :: thesis: for a being object holds
( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S1[a] ) & ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) )
let a be object ; :: thesis: ( ( a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) implies S1[a] ) & ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ) )
hereby :: thesis: ( S1[a] implies a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) )
assume a is Element of (Image ((ClImageMap L) | (DsupClOpers L))) ; :: thesis: S1[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 S1[a] ; :: thesis: verum
end;
assume S1[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;
A3: for a being object holds
( a is Element of ((Subalgebras L) opp) iff S1[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