let T be non empty reflexive RelStr ; :: thesis: sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in sigma T or s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
reconsider ss = s as set by TARSKI:1;
A1: ss \ (uparrow ({} T)) = s ;
assume s in sigma T ; :: thesis: s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
hence s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A1; :: thesis: verum