let A be set ; :: thesis: for a, b being Element of
for E1, E2 being Equivalence_Relation of st a = E1 & b = E2 holds
a "\/" b = E1 "\/" E2
let a, b be Element of ; :: thesis: for E1, E2 being Equivalence_Relation of st a = E1 & b = E2 holds
a "\/" b = E1 "\/" E2
let E1, E2 be Equivalence_Relation of ; :: thesis: ( a = E1 & b = E2 implies a "\/" b = E1 "\/" E2 )
assume A1: ( a = E1 & b = E2 ) ; :: thesis: a "\/" b = E1 "\/" E2
reconsider y = b as Element of ;
reconsider x = a as Element of ;
reconsider x = x as Element of ;
reconsider y = y as Element of ;
( % (x % ) = x % & % (y % ) = y % ) ;
hence a "\/" b = x "\/" y by Th9
.= the L_join of (EqRelLatt A) . x,y by LATTICES:def 1
.= E1 "\/" E2 by A1, MSUALG_5:def 2 ;
:: thesis: verum
reconsider a1 = a, b1 = b as Element of ;