let G be Group; :: thesis: for A, B being Subset of G st A c= B holds
A " c= B "
let A, B be Subset of G; :: thesis: ( A c= B implies A " c= B " )
assume A1: A c= B ; :: thesis: A " c= B "
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A " or a in B " )
assume a in A " ; :: thesis: a in B "
then ex g being Element of G st
( a = g " & g in A ) ;
hence a in B " by A1; :: thesis: verum