let T be 1-sorted ; :: thesis: for F being Subset-Family of T holds COMPLEMENT F = { (a `) where a is Subset of T : a in F }
let F be Subset-Family of T; :: thesis: COMPLEMENT F = { (a `) where a is Subset of T : a in F }
set X = { (a `) where a is Subset of T : a in F } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (a `) where a is Subset of T : a in F } c= COMPLEMENT F

let x be object ; :: thesis: ( x in COMPLEMENT F implies x in { (a `) where a is Subset of T : a in F } )
assume A1: x in COMPLEMENT F ; :: thesis: x in { (a `) where a is Subset of T : a in F }
then reconsider P = x as Subset of T ;
A2: P ` in F by A1, SETFAM_1:def 7;
(P `) ` = P ;
hence x in { (a `) where a is Subset of T : a in F } by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a `) where a is Subset of T : a in F } or x in COMPLEMENT F )
assume x in { (a `) where a is Subset of T : a in F } ; :: thesis: x in COMPLEMENT F
then ex P being Subset of T st
( x = P ` & P in F ) ;
hence x in COMPLEMENT F by YELLOW_8:5; :: thesis: verum