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_{2}(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_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))))
by Th27

.= H_{1}(A) $$ ((SUB (Bottom (NormForm A))),(H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))))
by LATTICE2:def 3

.= (H_{2}(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))) . (Bottom (NormForm A))
by A2, SETWISEO:17, ZFMISC_1:1

.= H_{2}(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

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

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

.= H

.= (H

.= H

.= mi (O ^ O) by A1, A3, NORMFORM:def 12

.= {[{},{}]} by Th3 ; :: thesis: verum