let S be non empty finite set ; :: thesis: for s being FinSequence of S holds whole_event = s " S
let s be FinSequence of S; :: thesis: whole_event = s " S
( s " S c= s " (rng s) & s " (rng s) c= s " S ) by RELAT_1:170, RELAT_1:178;
then s " (rng s) = s " S by XBOOLE_0:def 10;
hence whole_event = s " S by RELAT_1:169; :: thesis: verum