reconsider a = q `3_4 , b = q `4_4 as Element of L ;

set x = q `1_4 ;

set y = q `2_4 ;

defpred S_{1}[ 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 S_{1}[p,q,r]

A24: for p, q being Element of new_set A holds S_{1}[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 )

( 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)

( 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 )

( 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

set x = q `1_4 ;

set y = q `2_4 ;

defpred S

( 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 S

proof

consider f being Function of [:(new_set A),(new_set A):], the carrier of L such that
let p, q be Element of new_set A; :: thesis: ex r being Element of L st S_{1}[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}}}

end;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

A8:
not {{{A}}} in A
assume
{{A}} = {{{A}}}
; :: thesis: contradiction

then {{A}} in {{A}} by TARSKI:def 1;

hence contradiction ; :: thesis: verum

end;then {{A}} in {{A}} by TARSKI:def 1;

hence contradiction ; :: thesis: verum

proof

A11:
{A} <> {{{A}}}
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;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

proof

A12:
not {{A}} in A
assume
{A} = {{{A}}}
; :: thesis: contradiction

then {{A}} in {A} by TARSKI:def 1;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then {{A}} in {A} by TARSKI:def 1;

hence contradiction by TARSKI:def 1; :: thesis: verum

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;assume {{A}} in A ; :: thesis: contradiction

hence contradiction by A13, XREGULAR:7; :: thesis: verum

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;

end;

suppose
( p in A & q in A )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider p9 = p, q9 = q as Element of A ;

take d . (p9,q9) ; :: thesis: S_{1}[p,q,d . (p9,q9)]

thus S_{1}[p,q,d . (p9,q9)]
by A6, A12, A8; :: thesis: verum

end;take d . (p9,q9) ; :: thesis: S

thus S

suppose A14:
( ( p = {{A}} & q = {{{A}}} ) or ( q = {{A}} & p = {{{A}}} ) )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

end;

end;

suppose A15:
( ( p = {A} & q = {{A}} ) or ( q = {A} & p = {{A}} ) )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

take
b
; :: thesis: S_{1}[p,q,b]

thus S_{1}[p,q,b]
by A7, A11, A12, A15, TARSKI:def 1; :: thesis: verum

end;thus S

suppose A16:
( ( p = {A} & q = {{{A}}} ) or ( q = {A} & p = {{{A}}} ) )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

take
a "\/" b
; :: thesis: S_{1}[p,q,a "\/" b]

thus S_{1}[p,q,a "\/" b]
by A7, A11, A8, A16, TARSKI:def 1; :: thesis: verum

end;thus S

suppose A17:
( ( p = {A} or p = {{A}} or p = {{{A}}} ) & q = p )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

take
Bottom L
; :: thesis: S_{1}[p,q, Bottom L]

thus S_{1}[p,q, Bottom L]
by A7, A11, A12, A8, A17, TARSKI:def 1; :: thesis: verum

end;thus S

suppose A18:
( p in A & q = {A} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider p9 = p as Element of A ;

take (d . (p9,(q `1_4))) "\/" a ; :: thesis: S_{1}[p,q,(d . (p9,(q `1_4))) "\/" a]

thus S_{1}[p,q,(d . (p9,(q `1_4))) "\/" a]
by A11, A12, A8, A18, TARSKI:def 1; :: thesis: verum

end;take (d . (p9,(q `1_4))) "\/" a ; :: thesis: S

thus S

suppose A19:
( p in A & q = {{A}} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider p9 = p as Element of A ;

take ((d . (p9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S_{1}[p,q,((d . (p9,(q `1_4))) "\/" a) "\/" b]

thus S_{1}[p,q,((d . (p9,(q `1_4))) "\/" a) "\/" b]
by A7, A12, A8, A19, TARSKI:def 1; :: thesis: verum

end;take ((d . (p9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S

thus S

suppose A20:
( p in A & q = {{{A}}} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider p9 = p as Element of A ;

take (d . (p9,(q `2_4))) "\/" b ; :: thesis: S_{1}[p,q,(d . (p9,(q `2_4))) "\/" b]

thus S_{1}[p,q,(d . (p9,(q `2_4))) "\/" b]
by A7, A11, A12, A8, A20, TARSKI:def 1; :: thesis: verum

end;take (d . (p9,(q `2_4))) "\/" b ; :: thesis: S

thus S

suppose A21:
( q in A & p = {A} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider q9 = q as Element of A ;

take (d . (q9,(q `1_4))) "\/" a ; :: thesis: S_{1}[p,q,(d . (q9,(q `1_4))) "\/" a]

thus S_{1}[p,q,(d . (q9,(q `1_4))) "\/" a]
by A11, A12, A8, A21, TARSKI:def 1; :: thesis: verum

end;take (d . (q9,(q `1_4))) "\/" a ; :: thesis: S

thus S

suppose A22:
( q in A & p = {{A}} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider q9 = q as Element of A ;

take ((d . (q9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S_{1}[p,q,((d . (q9,(q `1_4))) "\/" a) "\/" b]

thus S_{1}[p,q,((d . (q9,(q `1_4))) "\/" a) "\/" b]
by A7, A12, A8, A22, TARSKI:def 1; :: thesis: verum

end;take ((d . (q9,(q `1_4))) "\/" a) "\/" b ; :: thesis: S

thus S

suppose A23:
( q in A & p = {{{A}}} )
; :: thesis: ex r being Element of L st S_{1}[p,q,r]

then reconsider q9 = q as Element of A ;

take (d . (q9,(q `2_4))) "\/" b ; :: thesis: S_{1}[p,q,(d . (q9,(q `2_4))) "\/" b]

thus S_{1}[p,q,(d . (q9,(q `2_4))) "\/" b]
by A7, A11, A12, A8, A23, TARSKI:def 1; :: thesis: verum

end;take (d . (q9,(q `2_4))) "\/" b ; :: thesis: S

thus S

A24: for p, q being Element of new_set A holds S

{{{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

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
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;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

( 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

for u being Element of A holds
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;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

( 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

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
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;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

( 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