let A be Tolerance_Space; :: thesis: for X, Y being Subset of A st X c= Y holds
LAp X c= LAp Y
let X, Y be Subset of A; :: thesis: ( X c= Y implies LAp X c= LAp Y )
assume A1: X c= Y ; :: thesis: LAp X c= LAp Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LAp X or x in LAp Y )
assume A2: x in LAp X ; :: thesis: x in LAp Y
then Class ( the InternalRel of A,x) c= X by Th8;
then Class ( the InternalRel of A,x) c= Y by A1;
hence x in LAp Y by A2; :: thesis: verum