let L be complete LATTICE; :: thesis: Image (() | ()) = () 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 (() | ())) implies S1[a] ) & ( S1[a] implies a is Element of (Image (() | ())) ) )
let a be object ; :: thesis: ( ( a is Element of (Image (() | ())) implies S1[a] ) & ( S1[a] implies a is Element of (Image (() | ())) ) )
hereby :: thesis: ( S1[a] implies a is Element of (Image (() | ())) )
assume a is Element of (Image (() | ())) ; :: thesis: S1[a]
then consider x being Element of () such that
A2: ((ClImageMap L) | ()) . x = a by YELLOW_2:10;
reconsider x = x as directed-sups-preserving closure Function of L,L by Th26;
a = () . x by
.= Image x by Def4 ;
hence S1[a] ; :: thesis: verum
end;
assume S1[a] ; :: thesis: a is Element of (Image (() | ()))
then reconsider S = a as strict closure directed-sups-inheriting System of L ;
reconsider x = closure_op S as Element of () by Th26;
S = Image () by Th18
.= () . () by Def4
.= (() | ()) . x by Th6 ;
then S in rng (() | ()) by FUNCT_2:4;
hence a is Element of (Image (() | ())) by YELLOW_0:def 15; :: thesis: verum
end;
A3: for a being object holds
( a is Element of (() opp) iff S1[a] ) by Th27;
RelStr(# the carrier of (Image (() | ())), the InternalRel of (Image (() | ())) #) = RelStr(# the carrier of (() opp), the InternalRel of (() opp) #) from hence Image (() | ()) = () opp ; :: thesis: verum