defpred S1[ object , object ] means ( Im (O,$1) = {} & $2 = $1 );
consider O1 being Relation such that
A1:
for a, b being object holds
( [a,b] in O1 iff ( a in X & b in X & S1[a,b] ) )
from RELAT_1:sch 1();
O1 c= [:X,X:]
then reconsider O1 = O1 as Operation of X ;
take
O1
; for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
let L be List of X; L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
thus
L | O1 c= union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
XBOOLE_0:def 10 union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } c= L | O1proof
let a be
object ;
TARSKI:def 3 ( not a in L | O1 or a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } )
assume
a in L | O1
;
a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
then consider b being
Element of
X such that A2:
(
a in b . O1 &
b in L )
by Th23;
[b,a] in O1
by A2, RELAT_1:169;
then A3:
(
a = b &
b . O = {} )
by A1;
then B1:
a in {b}
by TARSKI:def 1;
reconsider Z =
IFEQ (
(b . O),
{},
{b},
{}) as
set ;
A4:
a in Z
by A3, B1, FUNCOP_1:def 8;
IFEQ (
(b . O),
{},
{b},
{})
in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
by A2;
hence
a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
by A4, TARSKI:def 4;
verum
end;
let a be object ; TARSKI:def 3 ( not a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } or a in L | O1 )
assume
a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
; a in L | O1
then consider A being set such that
A5:
( a in A & A in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } )
by TARSKI:def 4;
consider x being Element of X such that
A6:
( A = IFEQ ((x . O),{},{x},{}) & x in L )
by A5;
A7:
x . O = {}
by A5, A6, FUNCOP_1:def 8;
then
A = {x}
by A6, FUNCOP_1:def 8;
then
a = x
by A5, TARSKI:def 1;
then
[x,a] in O1
by A1, A6, A7;
hence
a in L | O1
by A6, RELAT_1:def 13; verum