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