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