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) `)

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

hence
R is satisfying(7H')
; :: thesis: verum
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;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