let R be non empty RelStr ; :: thesis: ( ( for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) ` ) implies for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `) )
assume TR: for X being Subset of R holds UAp ((UAp X) `) c= (UAp X) ` ; :: thesis: for X being Subset of R holds (LAp X) ` c= LAp ((LAp X) `)
let X be Subset of R; :: thesis: (LAp X) ` c= LAp ((LAp X) `)
H1: LAp X = Lap X by ROUGHS_2:9
.= (UAp (X `)) ` by ROUGHS_2:def 9 ;
then ((UAp (X `)) `) ` c= (UAp (LAp X)) ` by TR, SUBSET_1:12;
then (LAp X) ` c= (Uap (LAp X)) ` by H1, ROUGHS_2:8;
then (LAp X) ` c= ((LAp ((LAp X) `)) `) ` by ROUGHS_2:def 8;
hence (LAp X) ` c= LAp ((LAp X) `) ; :: thesis: verum