reconsider a = q `3_4 , b = q `4_4 as Element of L ;
set x = q `1_4 ;
set y = q `2_4 ;
defpred S1[ Element of new_set A, Element of new_set A, Element of L] means ( ( $1 in A & $2 in A implies $3 = d . ($1,$2) ) & ( ( ( $1 = {{A}} & $2 = {{{A}}} ) or ( $2 = {{A}} & $1 = {{{A}}} ) ) implies $3 = a ) & ( ( ( $1 = {A} & $2 = {{A}} ) or ( $2 = {A} & $1 = {{A}} ) ) implies $3 = b ) & ( ( ( $1 = {A} & $2 = {{{A}}} ) or ( $2 = {A} & $1 = {{{A}}} ) ) implies $3 = a "\/" b ) & ( ( $1 = {A} or $1 = {{A}} or $1 = {{{A}}} ) & $2 = $1 implies $3 = Bottom L ) & ( $1 in A & $2 = {A} implies ex p9 being Element of A st
( p9 = $1 & $3 = (d . (p9,(q `1_4))) "\/" a ) ) & ( $1 in A & $2 = {{A}} implies ex p9 being Element of A st
( p9 = $1 & $3 = ((d . (p9,(q `1_4))) "\/" a) "\/" b ) ) & ( $1 in A & $2 = {{{A}}} implies ex p9 being Element of A st
( p9 = $1 & $3 = (d . (p9,(q `2_4))) "\/" b ) ) & ( $2 in A & $1 = {A} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . (q9,(q `1_4))) "\/" a ) ) & ( $2 in A & $1 = {{A}} implies ex q9 being Element of A st
( q9 = $2 & $3 = ((d . (q9,(q `1_4))) "\/" a) "\/" b ) ) & ( $2 in A & $1 = {{{A}}} implies ex q9 being Element of A st
( q9 = $2 & $3 = (d . (q9,(q `2_4))) "\/" b ) ) );
{{A}} in {{A},{{A}},{{{A}}}} by ENUMSET1:def 1;
then A1: {{A}} in new_set A by XBOOLE_0:def 3;
A2: for p, q being Element of new_set A ex r being Element of L st S1[p,q,r]
proof
let p, q be Element of new_set A; :: thesis: ex r being Element of L st S1[p,q,r]
A3: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A4: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A5: ( ( ( p = {A} or p = {{A}} or p = {{{A}}} ) & p = q ) iff ( ( p = {A} & q = {A} ) or ( p = {{A}} & q = {{A}} ) or ( p = {{{A}}} & q = {{{A}}} ) ) ) ;
A6: not {A} in A by TARSKI:def 1;
A7: {{A}} <> {{{A}}}
proof
assume {{A}} = {{{A}}} ; :: thesis: contradiction
then {{A}} in {{A}} by TARSKI:def 1;
hence contradiction ; :: thesis: verum
end;
A8: not {{{A}}} in A
proof
A9: {{A}} in {{{A}}} by TARSKI:def 1;
A10: ( A in {A} & {A} in {{A}} ) by TARSKI:def 1;
assume {{{A}}} in A ; :: thesis: contradiction
hence contradiction by A10, A9, XREGULAR:8; :: thesis: verum
end;
A11: {A} <> {{{A}}}
proof
assume {A} = {{{A}}} ; :: thesis: contradiction
then {{A}} in {A} by TARSKI:def 1;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
A12: not {{A}} in A
proof
A13: ( A in {A} & {A} in {{A}} ) by TARSKI:def 1;
assume {{A}} in A ; :: thesis: contradiction
hence contradiction by A13, XREGULAR:7; :: thesis: verum
end;
per cases ( ( p in A & q in A ) or ( p = {{A}} & q = {{{A}}} ) or ( q = {{A}} & p = {{{A}}} ) or ( p = {A} & q = {{A}} ) or ( q = {A} & p = {{A}} ) or ( p = {A} & q = {{{A}}} ) or ( q = {A} & p = {{{A}}} ) or ( ( p = {A} or p = {{A}} or p = {{{A}}} ) & q = p ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p in A & q = {{{A}}} ) or ( q in A & p = {A} ) or ( q in A & p = {{A}} ) or ( q in A & p = {{{A}}} ) ) by A3, A4, A5, ENUMSET1:def 1;
suppose ( p in A & q in A ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider p9 = p, q9 = q as Element of A ;
take d . (p9,q9) ; :: thesis: S1[p,q,d . (p9,q9)]
thus S1[p,q,d . (p9,q9)] by A6, A12, A8; :: thesis: verum
end;
suppose A14: ( ( p = {{A}} & q = {{{A}}} ) or ( q = {{A}} & p = {{{A}}} ) ) ; :: thesis: ex r being Element of L st S1[p,q,r]
take a ; :: thesis: S1[p,q,a]
thus S1[p,q,a] by A7, A11, A12, A8, A14; :: thesis: verum
end;
suppose A15: ( ( p = {A} & q = {{A}} ) or ( q = {A} & p = {{A}} ) ) ; :: thesis: ex r being Element of L st S1[p,q,r]
take b ; :: thesis: S1[p,q,b]
thus S1[p,q,b] by A7, A11, A12, A15, TARSKI:def 1; :: thesis: verum
end;
suppose A16: ( ( p = {A} & q = {{{A}}} ) or ( q = {A} & p = {{{A}}} ) ) ; :: thesis: ex r being Element of L st S1[p,q,r]
take a "\/" b ; :: thesis: S1[p,q,a "\/" b]
thus S1[p,q,a "\/" b] by A7, A11, A8, A16, TARSKI:def 1; :: thesis: verum
end;
suppose A17: ( ( p = {A} or p = {{A}} or p = {{{A}}} ) & q = p ) ; :: thesis: ex r being Element of L st S1[p,q,r]
take Bottom L ; :: thesis: S1[p,q, Bottom L]
thus S1[p,q, Bottom L] by A7, A11, A12, A8, A17, TARSKI:def 1; :: thesis: verum
end;
suppose A18: ( p in A & q = {A} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider p9 = p as Element of A ;
take (d . (p9,(q `1_4))) "\/" a ; :: thesis: S1[p,q,(d . (p9,(q `1_4))) "\/" a]
thus S1[p,q,(d . (p9,(q `1_4))) "\/" a] by A11, A12, A8, A18, TARSKI:def 1; :: thesis: verum
end;
suppose A19: ( p in A & q = {{A}} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider p9 = p as Element of A ;
take ((d . (p9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S1[p,q,((d . (p9,(q `1_4))) "\/" a) "\/" b]
thus S1[p,q,((d . (p9,(q `1_4))) "\/" a) "\/" b] by A7, A12, A8, A19, TARSKI:def 1; :: thesis: verum
end;
suppose A20: ( p in A & q = {{{A}}} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider p9 = p as Element of A ;
take (d . (p9,(q `2_4))) "\/" b ; :: thesis: S1[p,q,(d . (p9,(q `2_4))) "\/" b]
thus S1[p,q,(d . (p9,(q `2_4))) "\/" b] by A7, A11, A12, A8, A20, TARSKI:def 1; :: thesis: verum
end;
suppose A21: ( q in A & p = {A} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider q9 = q as Element of A ;
take (d . (q9,(q `1_4))) "\/" a ; :: thesis: S1[p,q,(d . (q9,(q `1_4))) "\/" a]
thus S1[p,q,(d . (q9,(q `1_4))) "\/" a] by A11, A12, A8, A21, TARSKI:def 1; :: thesis: verum
end;
suppose A22: ( q in A & p = {{A}} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider q9 = q as Element of A ;
take ((d . (q9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S1[p,q,((d . (q9,(q `1_4))) "\/" a) "\/" b]
thus S1[p,q,((d . (q9,(q `1_4))) "\/" a) "\/" b] by A7, A12, A8, A22, TARSKI:def 1; :: thesis: verum
end;
suppose A23: ( q in A & p = {{{A}}} ) ; :: thesis: ex r being Element of L st S1[p,q,r]
then reconsider q9 = q as Element of A ;
take (d . (q9,(q `2_4))) "\/" b ; :: thesis: S1[p,q,(d . (q9,(q `2_4))) "\/" b]
thus S1[p,q,(d . (q9,(q `2_4))) "\/" b] by A7, A11, A12, A8, A23, TARSKI:def 1; :: thesis: verum
end;
end;
end;
consider f being Function of [:(new_set A),(new_set A):], the carrier of L such that
A24: for p, q being Element of new_set A holds S1[p,q,f . (p,q)] from BINOP_1:sch 3(A2);
 {{{A}}} in {{A},{{A}},{{{A}}}} by ENUMSET1:def 1;
then A25: {{{A}}} in new_set A by XBOOLE_0:def 3;
reconsider f = f as BiFunction of (new_set A),L ;
{A} in {{A},{{A}},{{{A}}}} by ENUMSET1:def 1;
then A26: {A} in new_set A by XBOOLE_0:def 3;
A27: for u being Element of A holds
( f . ({A},u) = (d . (u,(q `1_4))) "\/" a & f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" b )
proof
let u be Element of A; :: thesis: ( f . ({A},u) = (d . (u,(q `1_4))) "\/" a & f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" b )
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . ({A},u9) = (d . (u1,(q `1_4))) "\/" a ) by A26, A24;
hence f . ({A},u) = (d . (u,(q `1_4))) "\/" a ; :: thesis: ( f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" b )
ex u2 being Element of A st
( u2 = u9 & f . ({{A}},u9) = ((d . (u2,(q `1_4))) "\/" a) "\/" b ) by A1, A24;
hence f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" a) "\/" b ; :: thesis: f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" b
ex u3 being Element of A st
( u3 = u9 & f . ({{{A}}},u9) = (d . (u3,(q `2_4))) "\/" b ) by A25, A24;
hence f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" b ; :: thesis: verum
end;
take f ; :: thesis: ( ( for u, v being Element of A holds f . (u,v) = d . (u,v) ) & f . ({A},{A}) = Bottom L & f . ({{A}},{{A}}) = Bottom L & f . ({{{A}}},{{{A}}}) = Bottom L & f . ({{A}},{{{A}}}) = q `3_4 & f . ({{{A}}},{{A}}) = q `3_4 & f . ({A},{{A}}) = q `4_4 & f . ({{A}},{A}) = q `4_4 & f . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & f . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( f . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) )
A28: for u, v being Element of A holds f . (u,v) = d . (u,v)
proof
let u, v be Element of A; :: thesis: f . (u,v) = d . (u,v)
reconsider u9 = u, v9 = v as Element of new_set A by XBOOLE_0:def 3;
thus f . (u,v) = f . (u9,v9)
.= d . (u,v) by A24 ; :: thesis: verum
end;
for u being Element of A holds
( f . (u,{A}) = (d . (u,(q `1_4))) "\/" a & f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" b )
proof
let u be Element of A; :: thesis: ( f . (u,{A}) = (d . (u,(q `1_4))) "\/" a & f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" b )
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st
( u1 = u9 & f . (u9,{A}) = (d . (u1,(q `1_4))) "\/" a ) by A26, A24;
hence f . (u,{A}) = (d . (u,(q `1_4))) "\/" a ; :: thesis: ( f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" a) "\/" b & f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" b )
ex u2 being Element of A st
( u2 = u9 & f . (u9,{{A}}) = ((d . (u2,(q `1_4))) "\/" a) "\/" b ) by A1, A24;
hence f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" a) "\/" b ; :: thesis: f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" b
ex u3 being Element of A st
( u3 = u9 & f . (u9,{{{A}}}) = (d . (u3,(q `2_4))) "\/" b ) by A25, A24;
hence f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" b ; :: thesis: verum
end;
hence ( ( for u, v being Element of A holds f . (u,v) = d . (u,v) ) & f . ({A},{A}) = Bottom L & f . ({{A}},{{A}}) = Bottom L & f . ({{{A}}},{{{A}}}) = Bottom L & f . ({{A}},{{{A}}}) = q `3_4 & f . ({{{A}}},{{A}}) = q `3_4 & f . ({A},{{A}}) = q `4_4 & f . ({{A}},{A}) = q `4_4 & f . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & f . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( f . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) by A26, A1, A25, A24, A28, A27; :: thesis: verum