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 that
A1: V1 c= W1 and
A2: V2 c= W2 ; :: thesis: V1 + V2 c= W1 + W2
let x be set ; :: 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 10;
then ex u, v being Point of X st
( u + v = x & u in V1 & v in V2 ) ;
then x in { (u' + v') where u', v' is Point of X : ( u' in W1 & v' in W2 ) } by A1, A2;
hence x in W1 + W2 by RUSUB_4:def 10; :: thesis: verum