let R be non empty mediate RelStr ; :: thesis: for X being Subset of R holds LAp (LAp X) c= LAp X
let X be Subset of R; :: thesis: LAp (LAp X) c= LAp X
A1: LAp (LAp X) = LAp (((LAp X) `) `)
.= (UAp ((LAp ((X `) `)) `)) ` by Th16
.= (UAp (((UAp (X `)) `) `)) ` by Th16
.= (UAp (UAp (X `))) ` ;
(UAp (X `)) ` = LAp ((X `) `) by Th16
.= LAp X ;
hence LAp (LAp X) c= LAp X by A1, SUBSET_1:12, Th39; :: thesis: verum