hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (F4(a) `) where a is Element of F1() : a in F3() } c= COMPLEMENT F2()
let x be object ; :: thesis: ( x in COMPLEMENT F2() implies x in { (F4(a) `) where a is Element of F1() : a in F3() } )
assume A2: x in COMPLEMENT F2() ; :: thesis: x in { (F4(a) `) where a is Element of F1() : a in F3() }
then reconsider y = x as Subset of F1() ;
y ` in F2() by A2, SETFAM_1:def 7;
then A3: ex b being Element of F1() st
( y ` = F4(b) & b in F3() ) by A1;
x = (y `) ` ;
hence x in { (F4(a) `) where a is Element of F1() : a in F3() } by A3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (F4(a) `) where a is Element of F1() : a in F3() } or x in COMPLEMENT F2() )
assume x in { (F4(a) `) where a is Element of F1() : a in F3() } ; :: thesis: x in COMPLEMENT F2()
then consider a being Element of F1() such that
A4: x = F4(a) ` and
A5: a in F3() ;
F4(a) in F2() by A1, A5;
hence x in COMPLEMENT F2() by A4, YELLOW_8:5; :: thesis: verum