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_fun2 (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_fun2 (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_fun2 (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_fun2 (d,q) is symmetric
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: new_bi_fun2 (d,q) is symmetric
set f = new_bi_fun2 (d,q);
set x = q `1 ;
set y = q `2 ;
set a = q `3 ;
set b = q `4 ;
let p, q be Element of new_set2 A; :: according to LATTICE5:def 5 :: thesis: (new_bi_fun2 (d,q)) . (p,q) = (new_bi_fun2 (d,q)) . (q,p)
A2: ( p in A or p in {{A},{{A}}} ) by XBOOLE_0:def 3;
A3: ( q in A or q in {{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 = {A} & q in 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}} ) ) by A2, A3, TARSKI:def 2;

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

then reconsider p9 = p, q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = d . (p9,q9) by Def5
.= d . (q9,p9) by A1, LATTICE5:def 5
.= (new_bi_fun2 (d,q)) . (q,p) by Def5 ; :: thesis: verum

end;

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

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

end;

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

then reconsider p9 = p as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (p9,(q `2))) "\/" (q `3) by A5, Def5
.= (new_bi_fun2 (d,q)) . (q,p) by A5, Def5 ; :: thesis: verum

end;

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

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `1))) "\/" (q `3) by A6, Def5
.= (new_bi_fun2 (d,q)) . (q,p) by A6, Def5 ; :: thesis: verum

end;

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

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

end;

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

hence (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) by Def5
.= (new_bi_fun2 (d,q)) . (q,p) by A7, Def5 ;
:: thesis: verum

end;

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

then reconsider q9 = q as Element of A ;
thus (new_bi_fun2 (d,q)) . (p,q) = (d . (q9,(q `2))) "\/" (q `3) by A8, Def5
.= (new_bi_fun2 (d,q)) . (q,p) by A8, Def5 ; :: thesis: verum

end;

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

hence (new_bi_fun2 (d,q)) . (p,q) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) by Def5
.= (new_bi_fun2 (d,q)) . (q,p) by A9, Def5 ;
:: thesis: verum

end;

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

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

end;

end;