let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for B1, B2 being Subset of T
for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
let B1, B2 be Subset of T; :: thesis: for p being Point of T st B1 c= B2 holds
B1 + p c= B2 + p
let p be Point of T; :: thesis: ( B1 c= B2 implies B1 + p c= B2 + p )
assume A1: B1 c= B2 ; :: thesis: B1 + p c= B2 + p
let p1 be object ; :: according to TARSKI:def 3 :: thesis: ( not p1 in B1 + p or p1 in B2 + p )
assume p1 in B1 + p ; :: thesis: p1 in B2 + p
then ex p2 being Point of T st
( p1 = p2 + p & p2 in B1 ) ;
hence p1 in B2 + p by A1; :: thesis: verum