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

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