let R be non empty finite RelStr ; :: thesis: ( R is satisfying(7L') implies R is satisfying(7H') )
assume tr: R is satisfying(7L') ; :: thesis: R is satisfying(7H')
for X being Subset of R holds (UAp X) ` c= UAp ((UAp X) `)

proof

let X be Subset of R; :: thesis: (UAp X) ` c= UAp ((UAp X) `)
H1: UAp X = Uap X by ROUGHS_2:8
.= (LAp (X `)) ` by ROUGHS_2:def 8 ;
then ((LAp (X `)) `) ` c= (LAp (UAp X)) ` by tr, SUBSET_1:12;
then (UAp X) ` c= (Lap (UAp X)) ` by H1, ROUGHS_2:9;
then (UAp X) ` c= ((UAp ((UAp X) `)) `) ` by ROUGHS_2:def 9;
hence (UAp X) ` c= UAp ((UAp X) `) ; :: thesis: verum

end;

hence R is satisfying(7H') ; :: thesis: verum