let X1, X2 be non empty set ; :: thesis: for A, B being Subset of [:X1,X2:]
for p being set holds
( X-section ((A \ B),p) = (X-section (A,p)) \ (X-section (B,p)) & Y-section ((A \ B),p) = (Y-section (A,p)) \ (Y-section (B,p)) )
let E1, E2 be Subset of [:X1,X2:]; :: thesis: for p being set holds
( X-section ((E1 \ E2),p) = (X-section (E1,p)) \ (X-section (E2,p)) & Y-section ((E1 \ E2),p) = (Y-section (E1,p)) \ (Y-section (E2,p)) )
let p be set ; :: thesis: ( X-section ((E1 \ E2),p) = (X-section (E1,p)) \ (X-section (E2,p)) & Y-section ((E1 \ E2),p) = (Y-section (E1,p)) \ (Y-section (E2,p)) )
now :: thesis: for q being set st q in X-section ((E1 \ E2),p) holds
q in (X-section (E1,p)) \ (X-section (E2,p))
let q be set ; :: thesis: ( q in X-section ((E1 \ E2),p) implies q in (X-section (E1,p)) \ (X-section (E2,p)) )
assume q in X-section ((E1 \ E2),p) ; :: thesis: q in (X-section (E1,p)) \ (X-section (E2,p))
then q in { y where y is Element of X2 : [p,y] in E1 \ E2 } by MEASUR11:def 4;
then A1: ex y being Element of X2 st
( q = y & [p,y] in E1 \ E2 ) ;
then ( [p,q] in E1 & not [p,q] in E2 ) by XBOOLE_0:def 5;
then q in { y where y is Element of X2 : [p,y] in E1 } by A1;
then A3: q in X-section (E1,p) by MEASUR11:def 4;
now :: thesis: not q in X-section (E2,p)
assume q in X-section (E2,p) ; :: thesis: contradiction
then q in { y where y is Element of X2 : [p,y] in E2 } by MEASUR11:def 4;
then ex y being Element of X2 st
( q = y & [p,y] in E2 ) ;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum
end;
hence q in (X-section (E1,p)) \ (X-section (E2,p)) by A3, XBOOLE_0:def 5; :: thesis: verum
end;
then A4: X-section ((E1 \ E2),p) c= (X-section (E1,p)) \ (X-section (E2,p)) ;
now :: thesis: for q being set st q in (X-section (E1,p)) \ (X-section (E2,p)) holds
q in X-section ((E1 \ E2),p)
let q be set ; :: thesis: ( q in (X-section (E1,p)) \ (X-section (E2,p)) implies q in X-section ((E1 \ E2),p) )
assume q in (X-section (E1,p)) \ (X-section (E2,p)) ; :: thesis: q in X-section ((E1 \ E2),p)
then ( q in X-section (E1,p) & not q in X-section (E2,p) ) by XBOOLE_0:def 5;
then A5: ( q in { y where y is Element of X2 : [p,y] in E1 } & not q in { y where y is Element of X2 : [p,y] in E2 } ) by MEASUR11:def 4;
then A6: ex y being Element of X2 st
( q = y & [p,y] in E1 ) ;
then not [p,q] in E2 by A5;
then [p,q] in E1 \ E2 by A6, XBOOLE_0:def 5;
then q in { y where y is Element of X2 : [p,y] in E1 \ E2 } by A6;
hence q in X-section ((E1 \ E2),p) by MEASUR11:def 4; :: thesis: verum
end;
then (X-section (E1,p)) \ (X-section (E2,p)) c= X-section ((E1 \ E2),p) ;
hence X-section ((E1 \ E2),p) = (X-section (E1,p)) \ (X-section (E2,p)) by A4; :: thesis: Y-section ((E1 \ E2),p) = (Y-section (E1,p)) \ (Y-section (E2,p))
now :: thesis: for q being set st q in Y-section ((E1 \ E2),p) holds
q in (Y-section (E1,p)) \ (Y-section (E2,p))
let q be set ; :: thesis: ( q in Y-section ((E1 \ E2),p) implies q in (Y-section (E1,p)) \ (Y-section (E2,p)) )
assume q in Y-section ((E1 \ E2),p) ; :: thesis: q in (Y-section (E1,p)) \ (Y-section (E2,p))
then q in { x where x is Element of X1 : [x,p] in E1 \ E2 } by MEASUR11:def 5;
then B1: ex x being Element of X1 st
( q = x & [x,p] in E1 \ E2 ) ;
then ( [q,p] in E1 & not [q,p] in E2 ) by XBOOLE_0:def 5;
then q in { x where x is Element of X1 : [x,p] in E1 } by B1;
then B3: q in Y-section (E1,p) by MEASUR11:def 5;
now :: thesis: not q in Y-section (E2,p)
assume q in Y-section (E2,p) ; :: thesis: contradiction
then q in { x where x is Element of X1 : [x,p] in E2 } by MEASUR11:def 5;
then ex x being Element of X1 st
( q = x & [x,p] in E2 ) ;
hence contradiction by B1, XBOOLE_0:def 5; :: thesis: verum
end;
hence q in (Y-section (E1,p)) \ (Y-section (E2,p)) by B3, XBOOLE_0:def 5; :: thesis: verum
end;
then B4: Y-section ((E1 \ E2),p) c= (Y-section (E1,p)) \ (Y-section (E2,p)) ;
now :: thesis: for q being set st q in (Y-section (E1,p)) \ (Y-section (E2,p)) holds
q in Y-section ((E1 \ E2),p)
let q be set ; :: thesis: ( q in (Y-section (E1,p)) \ (Y-section (E2,p)) implies q in Y-section ((E1 \ E2),p) )
assume q in (Y-section (E1,p)) \ (Y-section (E2,p)) ; :: thesis: q in Y-section ((E1 \ E2),p)
then ( q in Y-section (E1,p) & not q in Y-section (E2,p) ) by XBOOLE_0:def 5;
then B5: ( q in { x where x is Element of X1 : [x,p] in E1 } & not q in { x where x is Element of X1 : [x,p] in E2 } ) by MEASUR11:def 5;
then B6: ex x being Element of X1 st
( q = x & [x,p] in E1 ) ;
then not [q,p] in E2 by B5;
then [q,p] in E1 \ E2 by B6, XBOOLE_0:def 5;
then q in { x where x is Element of X1 : [x,p] in E1 \ E2 } by B6;
hence q in Y-section ((E1 \ E2),p) by MEASUR11:def 5; :: thesis: verum
end;
then (Y-section (E1,p)) \ (Y-section (E2,p)) c= Y-section ((E1 \ E2),p) ;
hence Y-section ((E1 \ E2),p) = (Y-section (E1,p)) \ (Y-section (E2,p)) by B4; :: thesis: verum