let R be non empty RelStr ; :: thesis: for A being Subset-Family of
for F being Subset of st A = { ((uparrow x) ` ) where x is Element of : x in F } holds
Intersect A = (uparrow F) `
deffunc H₁( Element of ) -> Element of bool the carrier of R = uparrow $1;
let A be Subset-Family of ; :: thesis: for F being Subset of st A = { ((uparrow x) ` ) where x is Element of : x in F } holds
Intersect A = (uparrow F) `
let F be Subset of ; :: thesis: ( A = { ((uparrow x) ` ) where x is Element of : x in F } implies Intersect A = (uparrow F) ` )
assume A1: A = { (H₁(x) ` ) where x is Element of : x in F } ; :: thesis: Intersect A = (uparrow F) `
A2: COMPLEMENT A = { H₁(x) where x is Element of : x in F } from YELLOW_9:sch 3(A1);
reconsider C = COMPLEMENT A as Subset-Family of ;
COMPLEMENT C = A ;
hence Intersect A = (union C) ` by YELLOW_8:15
.= (uparrow F) ` by A2, Th4 ;
:: thesis: verum