let A be set ; :: thesis: Top (NormForm A) = {[{},{}]}
reconsider O = {[{},{}]} as Element of Normal_forms_on A by Th17;
set sd = (StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)));
set F = H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))));
A1: @ ((pseudo_compl A) . (Bottom (NormForm A))) = mi (- (@ (Bottom (NormForm A)))) by Def8
.= mi O by Th13, NORMFORM:57
.= O by NORMFORM:42 ;
A2: Bottom (NormForm A) = {} by NORMFORM:57;
then (diff (Bottom (NormForm A))) . (Bottom (NormForm A)) = {} \ {} by Def11
.= Bottom (NormForm A) by NORMFORM:57 ;
then A3: @ (((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A))) = (StrongImpl A) . ((Bottom (NormForm A)),(Bottom (NormForm A))) by FUNCOP_1:48
.= mi ((@ (Bottom (NormForm A))) =>> (@ (Bottom (NormForm A)))) by Def9
.= mi O by A2, Th14
.= O by NORMFORM:42 ;
thus Top (NormForm A) = (Bottom (NormForm A)) => (Bottom (NormForm A)) by FILTER_0:28
.= FinJoin ((SUB (Bottom (NormForm A))),(H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))))))) by Th27
.= H₁(A) $$ ((SUB (Bottom (NormForm A))),(H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A))))))) by LATTICE2:def 3
.= (H₂(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))) . (Bottom (NormForm A)) by A2, SETWISEO:17, ZFMISC_1:1
.= H₂(A) . (((pseudo_compl A) . (Bottom (NormForm A))),(((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))) . (Bottom (NormForm A)))) by FUNCOP_1:37
.= mi (O ^ O) by A1, A3, NORMFORM:def 12
.= {[{},{}]} by Th3 ; :: thesis: verum