let A be set ; :: thesis: Top (NormForm A) = {[{} ,{} ]}
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: Bottom (NormForm A) = {} by NORMFORM:86;
A2: ( H₁(A) is commutative & H₁(A) is associative ) by LATTICE2:27, LATTICE2:29;
A3: (diff (Bottom (NormForm A))) . (Bottom (NormForm A)) = {} \ {} by A1, Def11
.= Bottom (NormForm A) by NORMFORM:86 ;
reconsider O = {[{} ,{} ]} as Element of Normal_forms_on A by Th22;
A4: @ ((pseudo_compl A) . (Bottom (NormForm A))) = mi (- (@ (Bottom (NormForm A)))) by Def8
.= mi O by Th18, NORMFORM:86
.= O by NORMFORM:66 ;
A5: @ (((StrongImpl A) [:] (diff (Bottom (NormForm A))),(Bottom (NormForm A))) . (Bottom (NormForm A))) = (StrongImpl A) . (Bottom (NormForm A)),(Bottom (NormForm A)) by A3, FUNCOP_1:60
.= mi ((@ (Bottom (NormForm A))) =>> (@ (Bottom (NormForm A)))) by Def9
.= mi O by A1, Th19
.= O by NORMFORM:66 ;
thus Top (NormForm A) = (Bottom (NormForm A)) => (Bottom (NormForm A)) by FILTER_0:38
.= FinJoin (SUB (Bottom (NormForm A))),(H₂(A) .: (pseudo_compl A),((StrongImpl A) [:] (diff (Bottom (NormForm A))),(Bottom (NormForm A)))) by Th33
.= 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 A1, A2, SETWISEO:26, 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:48
.= mi (O ^ O) by A4, A5, NORMFORM:def 14
.= {[{} ,{} ]} by Th7 ; :: thesis: verum