let A be set ; 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 = H2(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))),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))))
by Th27
.=
H1(A) $$ ((SUB (Bottom (NormForm A))),(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))))
by LATTICE2:def 3
.=
(H2(A) .: ((pseudo_compl A),((StrongImpl A) [:] ((diff (Bottom (NormForm A))),(Bottom (NormForm A)))))) . (Bottom (NormForm A))
by A2, SETWISEO:17, ZFMISC_1:1
.=
H2(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
; verum