let R be non empty RelStr ; :: thesis: for X, Y being Subset of R st X c= Y holds
LAp X c= LAp Y
let X, Y be Subset of R; :: thesis: ( X c= Y implies LAp X c= LAp Y )
assume A1: X c= Y ; :: thesis: LAp X c= LAp Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in LAp X or y in LAp Y )
assume y in LAp X ; :: thesis: y in LAp Y
then consider z being Element of R such that
A2: ( z = y & Class ( the InternalRel of R,z) c= X ) ;
Class ( the InternalRel of R,z) c= Y by A1, A2;
hence y in LAp Y by A2; :: thesis: verum