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

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