let X, x be set ; :: thesis: for F being Dependency-set of X holds
( x in saturated-subsets F iff ex B, A being Subset of X st
( x = B & A ^|^ B,F ) )
let F be Dependency-set of X; :: thesis: ( x in saturated-subsets F iff ex B, A being Subset of X st
( x = B & A ^|^ B,F ) )
hereby :: thesis: ( ex B, A being Subset of X st
( x = B & A ^|^ B,F ) implies x in saturated-subsets F )
assume x in saturated-subsets F ; :: thesis: ex B, A being Subset of X st
( x = B & A ^|^ B,F )
then consider B being Subset of X such that
A1: x = B and
A2: ex A being Subset of X st A ^|^ B,F ;
consider A being Subset of X such that
A3: A ^|^ B,F by A2;
take B = B; :: thesis: ex A being Subset of X st
( x = B & A ^|^ B,F )
take A = A; :: thesis: ( x = B & A ^|^ B,F )
thus ( x = B & A ^|^ B,F ) by A1, A3; :: thesis: verum
end;
given B, A being Subset of X such that A4: x = B and
A5: A ^|^ B,F ; :: thesis: x in saturated-subsets F
thus x in saturated-subsets F by A4, A5; :: thesis: verum