let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((B '/\' C) '/\' D) '/\' E or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A20: x in ((B '/\' C) '/\' D) '/\' E ; :: thesis: x in '/\' (G \ {A})
then A21: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}} by A20, PARTIT1:def 4;
then consider bcd, e being set such that
A22: bcd in (B '/\' C) '/\' D and
A23: e in E and
A24: x = bcd /\ e by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ {{}} by A22, PARTIT1:def 4;
then consider bc, d being set such that
A25: bc in B '/\' C and
A26: d in D and
A27: bcd = bc /\ d by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ {{}} by A25, PARTIT1:def 4;
then consider b, c being set such that
A28: b in B and
A29: c in C and
A30: bc = b /\ c by SETFAM_1:def 5;
set h = (((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e);
A32: C in dom (C .--> c) by TARSKI:def 1;
A34: D in dom (D .--> d) by TARSKI:def 1;
A35: not C in dom (D .--> d) by A12, TARSKI:def 1;
E in dom (E .--> e) by TARSKI:def 1;
then A37: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = (E .--> e) . E by FUNCT_4:13;
then A38: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E = e by FUNCOP_1:72;
not C in dom (E .--> e) by A12, TARSKI:def 1;
then ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C by FUNCT_4:11;
then ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = ((B .--> b) +* (C .--> c)) . C by A35, FUNCT_4:11;
then A39: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = (C .--> c) . C by A32, FUNCT_4:13;
then A40: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C = c by FUNCOP_1:72;
not D in dom (E .--> e) by A12, TARSKI:def 1;
then ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D by FUNCT_4:11;
then A41: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = (D .--> d) . D by A34, FUNCT_4:13;
then A42: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D = d by FUNCOP_1:72;
A43: not B in dom (C .--> c) by A12, TARSKI:def 1;
A44: not B in dom (D .--> d) by A12, TARSKI:def 1;
not B in dom (E .--> e) by A12, TARSKI:def 1;
then ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B by FUNCT_4:11;
then ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = ((B .--> b) +* (C .--> c)) . B by A44, FUNCT_4:11;
then A45: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = (B .--> b) . B by A43, FUNCT_4:11;
then A46: ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B = b by FUNCOP_1:72;
A47: for p being set st p in G \ {A} holds
((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . p in p dom ((B .--> b) +* (C .--> c)) = (dom (B .--> b)) \/ (dom (C .--> c)) by FUNCT_4:def 1;
then dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = ((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d)) by FUNCT_4:def 1;
then A49: dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) = (((dom (B .--> b)) \/ (dom (C .--> c))) \/ (dom (D .--> d))) \/ (dom (E .--> e)) by FUNCT_4:def 1;
A50: dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) = (({B} \/ {C}) \/ {D}) \/ {E} by A49
.= ({B,C} \/ {D}) \/ {E} by ENUMSET1:1
.= {B,C,D} \/ {E} by ENUMSET1:3
.= {B,C,D,E} by ENUMSET1:6 ;
then A51: D in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) by ENUMSET1:def 2;
A52: rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) c= bool Y then reconsider F = rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) as Subset-Family of Y ;
A56: C in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) by A50, ENUMSET1:def 2;
A57: E in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) by A50, ENUMSET1:def 2;
A58: B in dom ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) by A50, ENUMSET1:def 2;
A59: {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} c= rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) then A61: {(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . D),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . B),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . C),(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) . E)} = rng ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) by A52, XBOOLE_0:def 10;
reconsider h = (((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e) as Function ;
A62: xx c= Intersect F A69: rng h <> {} by A51, FUNCT_1:3;
Intersect F c= xx then x = Intersect F by A62, XBOOLE_0:def 10;
hence x in '/\' (G \ {A}) by A18, A17, A50, A47, A21, BVFUNC_2:def 1; :: thesis: verum