thus { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } c= { F3(F4(a)) where a is Element of F1() : P1[a] } :: according to XBOOLE_0:def 10 :: thesis: { F3(F4(a)) where a is Element of F1() : P1[a] } c= { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } or x in { F3(F4(a)) where a is Element of F1() : P1[a] } )
assume x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } ; :: thesis: x in { F3(F4(a)) where a is Element of F1() : P1[a] }
then consider a being Element of F2() such that
A1: x = F3(a) and
A2: a in { F4(b) where b is Element of F1() : P1[b] } ;
ex b being Element of F1() st
( a = F4(b) & P1[b] ) by A2;
hence x in { F3(F4(a)) where a is Element of F1() : P1[a] } by A1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F3(F4(a)) where a is Element of F1() : P1[a] } or x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } )
assume x in { F3(F4(a)) where a is Element of F1() : P1[a] } ; :: thesis: x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } }
then consider a being Element of F1() such that
A3: x = F3(F4(a)) and
A4: P1[a] ;
F4(a) in { F4(b) where b is Element of F1() : P1[b] } by A4;
hence x in { F3(a) where a is Element of F2() : a in { F4(b) where b is Element of F1() : P1[b] } } by A3; :: thesis: verum