let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (f EU g) = lfp (S,(TransEU (f,g)))
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (f EU g) = lfp (S,(TransEU (f,g)))
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (f EU g) = lfp (S,(TransEU (f,g)))
let f, g be Assign of (BASSModel (R,BASSIGN)); :: thesis: SIGMA (f EU g) = lfp (S,(TransEU (f,g)))
set h = f EU g;
set p = Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN);
A1: SIGMA (Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN)) = lfp (S,(TransEU (f,g))) by Th32;
lfp (S,(TransEU (f,g))) is_a_fixpoint_of TransEU (f,g) by KNASTER:4;
then A2: for s being Element of S holds
( s |= Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN) iff s |= Foax (g,f,(Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN))) ) by A1, Th48;
A3: SIGMA (f EU g) c= SIGMA (Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SIGMA (f EU g) or x in SIGMA (Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN)) )
assume x in SIGMA (f EU g) ; :: thesis: x in SIGMA (Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN))
then consider s being Element of S such that
A4: x = s and
A5: s |= f EU g ;
s |= Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN) by A2, A5, Th47;
hence x in SIGMA (Tau ((lfp (S,(TransEU (f,g)))),R,BASSIGN)) by A4; :: thesis: verum

end;

for s being Element of S holds
( s |= f EU g iff s |= Foax (g,f,(f EU g)) ) by Th46;
then SIGMA (f EU g) is_a_fixpoint_of TransEU (f,g) by Th48;
then lfp (S,(TransEU (f,g))) c= SIGMA (f EU g) by KNASTER:8;
hence SIGMA (f EU g) = lfp (S,(TransEU (f,g))) by A1, A3, XBOOLE_0:def 10; :: thesis: verum