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