let R be non empty finite RelStr ; :: thesis: ( R is satisfying(7H') implies R is serial )
set U = UAp R;
assume tr: R is satisfying(7H') ; :: thesis: R is serial
(UAp ({} R)) ` = [#] R ;
then Y2: [#] R c= UAp ([#] R) by tr;
FF: (UAp R) . ([#] R) = UAp ([#] R) by ROUGHS_2:def 11
.= the carrier of R by Y2, XBOOLE_0:def 10 ;
FO: (UAp R) . {} = UAp ({} R) by ROUGHS_2:def 11
.= {} ;
for X, Y being Subset of R holds (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y)
proof
let X, Y be Subset of R; :: thesis: (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y)
(UAp R) . (X \/ Y) = UAp (X \/ Y) by ROUGHS_2:def 11
.= (UAp X) \/ (UAp Y) by ROUGHS_2:13
.= ((UAp R) . X) \/ (UAp Y) by ROUGHS_2:def 11
.= ((UAp R) . X) \/ ((UAp R) . Y) by ROUGHS_2:def 11 ;
hence (UAp R) . (X \/ Y) = ((UAp R) . X) \/ ((UAp R) . Y) ; :: thesis: verum
end;
then consider S being non empty finite serial RelStr such that
H1: ( the carrier of S = the carrier of R & UAp R = UAp S ) by ROUGHS_2:32, FF, FO;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by Corr3A, H1;
hence R is serial by NatDay; :: thesis: verum