let S be non empty RelStr ; :: thesis: for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)
let x, t be Element of S; :: thesis: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (x "/\") " (downarrow t) c= { s where s is Element of S : x "/\" s <= t }
let a be object ; :: thesis: ( a in { s where s is Element of S : x "/\" s <= t } implies a in (x "/\") " (downarrow t) )
assume a in { s where s is Element of S : x "/\" s <= t } ; :: thesis: a in (x "/\") " (downarrow t)
then consider s being Element of S such that
A1: a = s and
A2: x "/\" s <= t ;
(x "/\") . s <= t by A2, Def18;
then (x "/\") . s in downarrow t by WAYBEL_0:17;
hence a in (x "/\") " (downarrow t) by A1, FUNCT_2:38; :: thesis: verum
end;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in (x "/\") " (downarrow t) or s in { s where s is Element of S : x "/\" s <= t } )
assume A3: s in (x "/\") " (downarrow t) ; :: thesis: s in { s where s is Element of S : x "/\" s <= t }
then reconsider s = s as Element of S ;
(x "/\") . s in downarrow t by A3, FUNCT_2:38;
then x "/\" s in downarrow t by Def18;
then x "/\" s <= t by WAYBEL_0:17;
hence s in { s where s is Element of S : x "/\" s <= t } ; :: thesis: verum