let R be non empty RelStr ; :: thesis: for X being Subset of R holds Lap X = LAp X
let X be Subset of R; :: thesis: Lap X = LAp X
Uap (X `) = UAp (X `) by Th8;
hence Lap X = LAp X ; :: thesis: verum