let S be non empty finite set ; :: thesis: for s being FinSequence of S
for e being set st e in whole_event holds
ex x being Element of S st e in event_pick x,s
let s be FinSequence of S; :: thesis: for e being set st e in whole_event holds
ex x being Element of S st e in event_pick x,s
let e be set ; :: thesis: ( e in whole_event implies ex x being Element of S st e in event_pick x,s )
assume A1: e in whole_event ; :: thesis: ex x being Element of S st e in event_pick x,s
then e in s " S by Th1;
then s . e in S by FUNCT_1:def 13;
then consider x being Element of S such that
A2: x = s . e ;
take x ; :: thesis: e in event_pick x,s
x in {x} by TARSKI:def 1;
hence e in event_pick x,s by A1, A2, FUNCT_1:def 13; :: thesis: verum