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