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)

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

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

then consider S being non empty finite serial RelStr such that
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;(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

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