defpred S₁[ set , set ] means ( P₁[$1] & P₂[$2] );
A2: for x being Element of F₂()
for y being Element of F₃() holds
( S₁[x,y] iff S₁[x,y] ) ;
A3: for x being Element of F₂()
for y being Element of F₃() st S₁[x,y] holds
F₄(x,y) = F₅(x,y) by A1;
A4: { F₄(x9,y9) where x9 is Element of F₂(), y9 is Element of F₃() : S₁[x9,y9] } = { F₅(x,y) where x is Element of F₂(), y is Element of F₃() : S₁[x,y] } from LFUZZY_0:sch 4(A2, A3);
A5: "\/" ( { ("\/" ( { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁())) where x is Element of F₂() : P₁[x] } ,F₁()) = "\/" ( { F₄(x,y) where x is Element of F₂(), y is Element of F₃() : ( P₁[x] & P₂[y] ) } ,F₁()) from LFUZZY_0:sch 1();
"\/" ( { ("\/" ( { F₅(x9,y9) where x9 is Element of F₂() : P₁[x9] } ,F₁())) where y9 is Element of F₃() : P₂[y9] } ,F₁()) = "\/" ( { F₅(x9,y9) where x9 is Element of F₂(), y9 is Element of F₃() : ( P₁[x9] & P₂[y9] ) } ,F₁()) from LFUZZY_0:sch 2()
.= "\/" ( { F₄(x9,y9) where x9 is Element of F₂(), y9 is Element of F₃() : ( P₁[x9] & P₂[y9] ) } ,F₁()) by A4 ;
hence "\/" ( { ("\/" ( { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁())) where x is Element of F₂() : P₁[x] } ,F₁()) = "\/" ( { ("\/" ( { F₅(x9,y9) where x9 is Element of F₂() : P₁[x9] } ,F₁())) where y9 is Element of F₃() : P₂[y9] } ,F₁()) by A5; :: thesis: verum