let L be non empty doubleLoopStr ; :: thesis: for A, B being non empty Subset of L st A c= B holds
A -Ideal c= B -Ideal
let A, B be non empty Subset of L; :: thesis: ( A c= B implies A -Ideal c= B -Ideal )
assume A1: A c= B ; :: thesis: A -Ideal c= B -Ideal
B c= B -Ideal by Def14;
then A c= B -Ideal by A1;
hence A -Ideal c= B -Ideal by Def14; :: thesis: verum