let R be non empty transitive mediate RelStr ; :: thesis: for X being Subset of R holds LAp X = LAp (LAp X)
let X be Subset of R; :: thesis: LAp X = LAp (LAp X)
A0: LAp X c= LAp (LAp X) by Th95L;
LAp (LAp X) c= LAp X by ROUGHS_2:40;
hence LAp X = LAp (LAp X) by A0, XBOOLE_0:def 10; :: thesis: verum