let L be non empty reflexive RelStr ; :: thesis: sigma L c= xi L
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sigma L or x in xi L )
assume x in sigma L ; :: thesis: x in xi L
hence x in xi L by WAYBEL28:29; :: thesis: verum