let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric
let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric )
assume A1: d is symmetric ; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: new_bi_fun (d,q) is symmetric
set f = new_bi_fun (d,q);
set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
set b = q `4_4 ;
let p, q be Element of new_set A; :: according to LATTICE5:def 5 :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)
A2: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A3: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;

per cases ( ( p in A & q in A ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p in A & q = {{{A}}} ) or ( p = {A} & q in A ) or ( p = {A} & q = {A} ) or ( p = {A} & q = {{A}} ) or ( p = {A} & q = {{{A}}} ) or ( p = {{A}} & q in A ) or ( p = {{A}} & q = {A} ) or ( p = {{A}} & q = {{A}} ) or ( p = {{A}} & q = {{{A}}} ) or ( p = {{{A}}} & q in A ) or ( p = {{{A}}} & q = {A} ) or ( p = {{{A}}} & q = {{A}} ) or ( p = {{{A}}} & q = {{{A}}} ) ) by A2, A3, ENUMSET1:def 1;

suppose ( p in A & q in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider p9 = p, q9 = q as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = d . (p9,q9) by Def10
.= d . (q9,p9) by A1
.= (new_bi_fun (d,q)) . (q,p) by Def10 ; :: thesis: verum

end;

suppose A4: ( p in A & q = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider p9 = p as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `1_4))) "\/" (q `3_4) by A4, Def10
.= (new_bi_fun (d,q)) . (q,p) by A4, Def10 ; :: thesis: verum

end;

suppose A5: ( p in A & q = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider p9 = p as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = ((d . (p9,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) by A5, Def10
.= (new_bi_fun (d,q)) . (q,p) by A5, Def10 ; :: thesis: verum

end;

suppose A6: ( p in A & q = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider p9 = p as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = (d . (p9,(q `2_4))) "\/" (q `4_4) by A6, Def10
.= (new_bi_fun (d,q)) . (q,p) by A6, Def10 ; :: thesis: verum

end;

suppose A7: ( p = {A} & q in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider q9 = q as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = (d . (q9,(q `1_4))) "\/" (q `3_4) by A7, Def10
.= (new_bi_fun (d,q)) . (q,p) by A7, Def10 ; :: thesis: verum

end;

suppose ( p = {A} & q = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p) ; :: thesis: verum

end;

suppose A8: ( p = {A} & q = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = q `4_4 by Def10
.= (new_bi_fun (d,q)) . (q,p) by A8, Def10 ;
:: thesis: verum

end;

suppose A9: ( p = {A} & q = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = (q `3_4) "\/" (q `4_4) by Def10
.= (new_bi_fun (d,q)) . (q,p) by A9, Def10 ;
:: thesis: verum

end;

suppose A10: ( p = {{A}} & q in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider q9 = q as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = ((d . (q9,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) by A10, Def10
.= (new_bi_fun (d,q)) . (q,p) by A10, Def10 ; :: thesis: verum

end;

suppose A11: ( p = {{A}} & q = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = q `4_4 by Def10
.= (new_bi_fun (d,q)) . (q,p) by A11, Def10 ;
:: thesis: verum

end;

suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p) ; :: thesis: verum

end;

suppose A12: ( p = {{A}} & q = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = q `3_4 by Def10
.= (new_bi_fun (d,q)) . (q,p) by A12, Def10 ;
:: thesis: verum

end;

suppose A13: ( p = {{{A}}} & q in A ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

then reconsider q9 = q as Element of A ;
thus (new_bi_fun (d,q)) . (p,q) = (d . (q9,(q `2_4))) "\/" (q `4_4) by A13, Def10
.= (new_bi_fun (d,q)) . (q,p) by A13, Def10 ; :: thesis: verum

end;

suppose A14: ( p = {{{A}}} & q = {A} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = (q `3_4) "\/" (q `4_4) by Def10
.= (new_bi_fun (d,q)) . (q,p) by A14, Def10 ;
:: thesis: verum

end;

suppose A15: ( p = {{{A}}} & q = {{A}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = q `3_4 by Def10
.= (new_bi_fun (d,q)) . (q,p) by A15, Def10 ;
:: thesis: verum

end;

suppose ( p = {{{A}}} & q = {{{A}}} ) ; :: thesis: (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p)

hence (new_bi_fun (d,q)) . (p,q) = (new_bi_fun (d,q)) . (q,p) ; :: thesis: verum

end;

end;