let T be 1-sorted ; :: thesis: for F being Subset-Family of T
for X being set st X c= F holds
X is Subset-Family of T
let F be Subset-Family of T; :: thesis: for X being set st X c= F holds
X is Subset-Family of T
let X be set ; :: thesis: ( X c= F implies X is Subset-Family of T )
assume A1: X c= F ; :: thesis: X is Subset-Family of T
X c= bool the carrier of T

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in bool the carrier of T )
assume y in X ; :: thesis: y in bool the carrier of T
then y in F by A1;
hence y in bool the carrier of T ; :: thesis: verum

end;

hence X is Subset-Family of T ; :: thesis: verum