let RLS be non empty RLSStruct ; :: thesis: for Kr being SimplicialComplexStr of RLS
for A being Subset of Kr st not A is dependent holds
conv (@ A) c= |.Kr.|
let Kr be SimplicialComplexStr of RLS; :: thesis: for A being Subset of Kr st not A is dependent holds
conv (@ A) c= |.Kr.|
let A be Subset of Kr; :: thesis: ( not A is dependent implies conv (@ A) c= |.Kr.| )
assume A1: not A is dependent ; :: thesis: conv (@ A) c= |.Kr.|
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in conv (@ A) or x in |.Kr.| )
thus ( not x in conv (@ A) or x in |.Kr.| ) by A1, Def3; :: thesis: verum