set C = the non empty set ;
set f = the closure Function of (bool the non empty set ),(bool the non empty set );
take 1stOpStr(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ) #) ; :: thesis: ( 1stOpStr(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ) #) is with_closure & not 1stOpStr(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ) #) is empty )
thus ( 1stOpStr(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ) #) is with_closure & not 1stOpStr(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ) #) is empty ) ; :: thesis: verum