let X be non empty addLoopStr ; :: thesis: for V1, V2, W1, W2 being Subset of X st V1 c= W1 & V2 c= W2 holds
V1 + V2 c= W1 + W2
let V1, V2, W1, W2 be Subset of X; :: thesis: ( V1 c= W1 & V2 c= W2 implies V1 + V2 c= W1 + W2 )
assume A1: ( V1 c= W1 & V2 c= W2 ) ; :: thesis: V1 + V2 c= W1 + W2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V1 + V2 or x in W1 + W2 )
assume x in V1 + V2 ; :: thesis: x in W1 + W2
then x in { (u + v) where u, v is Point of X : ( u in V1 & v in V2 ) } by RUSUB_4:def 9;
then ex u, v being Point of X st
( u + v = x & u in V1 & v in V2 ) ;
then x in { (u9 + v9) where u9, v9 is Point of X : ( u9 in W1 & v9 in W2 ) } by A1;
hence x in W1 + W2 by RUSUB_4:def 9; :: thesis: verum