let L be LATTICE; :: thesis: for a, b being Element of L st L is modular holds

subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

let a, b be Element of L; :: thesis: ( L is modular implies subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic )

assume A1: L is modular ; :: thesis: subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

defpred S_{1}[ object , object ] means ( $2 is Element of L & ( for X, Y being Element of L st $1 = X & $2 = Y holds

Y = X "/\" a ) );

A2: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds

ex y being object st

( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S_{1}[x,y] )

A5: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A2);

reconsider f = f as Function of (subrelstr [#b,(a "\/" b)#]),(subrelstr [#(a "/\" b),a#]) ;

take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic

thus f is isomorphic :: thesis: verum

subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

let a, b be Element of L; :: thesis: ( L is modular implies subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic )

assume A1: L is modular ; :: thesis: subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

defpred S

Y = X "/\" a ) );

A2: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds

ex y being object st

( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S

proof

consider f being Function of the carrier of (subrelstr [#b,(a "\/" b)#]), the carrier of (subrelstr [#(a "/\" b),a#]) such that
let x be object ; :: thesis: ( x in the carrier of (subrelstr [#b,(a "\/" b)#]) implies ex y being object st

( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S_{1}[x,y] ) )

assume x in the carrier of (subrelstr [#b,(a "\/" b)#]) ; :: thesis: ex y being object st

( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S_{1}[x,y] )

then A3: x in [#b,(a "\/" b)#] by YELLOW_0:def 15;

then reconsider x1 = x as Element of L ;

take y = a "/\" x1; :: thesis: ( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S_{1}[x,y] )

x1 <= a "\/" b by A3, Def4;

then y <= a "/\" (a "\/" b) by YELLOW_5:6;

then A4: y <= a by LATTICE3:18;

b <= x1 by A3, Def4;

then a "/\" b <= y by YELLOW_5:6;

then y in [#(a "/\" b),a#] by A4, Def4;

hence y in the carrier of (subrelstr [#(a "/\" b),a#]) by YELLOW_0:def 15; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S

assume x in the carrier of (subrelstr [#b,(a "\/" b)#]) ; :: thesis: ex y being object st

( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S

then A3: x in [#b,(a "\/" b)#] by YELLOW_0:def 15;

then reconsider x1 = x as Element of L ;

take y = a "/\" x1; :: thesis: ( y in the carrier of (subrelstr [#(a "/\" b),a#]) & S

x1 <= a "\/" b by A3, Def4;

then y <= a "/\" (a "\/" b) by YELLOW_5:6;

then A4: y <= a by LATTICE3:18;

b <= x1 by A3, Def4;

then a "/\" b <= y by YELLOW_5:6;

then y in [#(a "/\" b),a#] by A4, Def4;

hence y in the carrier of (subrelstr [#(a "/\" b),a#]) by YELLOW_0:def 15; :: thesis: S

thus S

A5: for x being object st x in the carrier of (subrelstr [#b,(a "\/" b)#]) holds

S

reconsider f = f as Function of (subrelstr [#b,(a "\/" b)#]),(subrelstr [#(a "/\" b),a#]) ;

take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic

thus f is isomorphic :: thesis: verum

proof

A6:
b <= a "\/" b
by YELLOW_0:22;

b <= b ;

then b in [#b,(a "\/" b)#] by A6, Def4;

then reconsider s1 = subrelstr [#b,(b "\/" a)#] as non empty full Sublattice of L by YELLOW_0:def 15;

A7: a "/\" b <= a by YELLOW_0:23;

a "/\" b <= a "/\" b ;

then a "/\" b in [#(a "/\" b),a#] by A7, Def4;

then reconsider s2 = subrelstr [#(a "/\" b),a#] as non empty full Sublattice of L by YELLOW_0:def 15;

reconsider f1 = f as Function of s1,s2 ;

dom f1 = the carrier of (subrelstr [#b,(a "\/" b)#]) by FUNCT_2:def 1;

then A8: dom f1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;

the carrier of (subrelstr [#(a "/\" b),a#]) c= rng f1

A16: for x, y being Element of s1 holds

( x <= y iff f1 . x <= f1 . y )

end;b <= b ;

then b in [#b,(a "\/" b)#] by A6, Def4;

then reconsider s1 = subrelstr [#b,(b "\/" a)#] as non empty full Sublattice of L by YELLOW_0:def 15;

A7: a "/\" b <= a by YELLOW_0:23;

a "/\" b <= a "/\" b ;

then a "/\" b in [#(a "/\" b),a#] by A7, Def4;

then reconsider s2 = subrelstr [#(a "/\" b),a#] as non empty full Sublattice of L by YELLOW_0:def 15;

reconsider f1 = f as Function of s1,s2 ;

dom f1 = the carrier of (subrelstr [#b,(a "\/" b)#]) by FUNCT_2:def 1;

then A8: dom f1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;

the carrier of (subrelstr [#(a "/\" b),a#]) c= rng f1

proof

then A15:
rng f1 = the carrier of (subrelstr [#(a "/\" b),a#])
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (subrelstr [#(a "/\" b),a#]) or y in rng f1 )

assume y in the carrier of (subrelstr [#(a "/\" b),a#]) ; :: thesis: y in rng f1

then A9: y in [#(a "/\" b),a#] by YELLOW_0:def 15;

then reconsider Y = y as Element of L ;

A10: a "/\" b <= Y by A9, Def4;

then (a "/\" b) "\/" b <= Y "\/" b by WAYBEL_1:2;

then A11: b <= Y "\/" b by LATTICE3:17;

A12: Y <= a by A9, Def4;

then Y "\/" b <= a "\/" b by WAYBEL_1:2;

then A13: Y "\/" b in [#b,(a "\/" b)#] by A11, Def4;

then A14: Y "\/" b in the carrier of (subrelstr [#b,(a "\/" b)#]) by YELLOW_0:def 15;

then reconsider f1yb = f1 . (Y "\/" b) as Element of L by A5;

f1yb = (Y "\/" b) "/\" a by A5, A14

.= Y "\/" (b "/\" a) by A1, A12

.= Y by A10, YELLOW_5:8 ;

hence y in rng f1 by A8, A13, FUNCT_1:def 3; :: thesis: verum

end;assume y in the carrier of (subrelstr [#(a "/\" b),a#]) ; :: thesis: y in rng f1

then A9: y in [#(a "/\" b),a#] by YELLOW_0:def 15;

then reconsider Y = y as Element of L ;

A10: a "/\" b <= Y by A9, Def4;

then (a "/\" b) "\/" b <= Y "\/" b by WAYBEL_1:2;

then A11: b <= Y "\/" b by LATTICE3:17;

A12: Y <= a by A9, Def4;

then Y "\/" b <= a "\/" b by WAYBEL_1:2;

then A13: Y "\/" b in [#b,(a "\/" b)#] by A11, Def4;

then A14: Y "\/" b in the carrier of (subrelstr [#b,(a "\/" b)#]) by YELLOW_0:def 15;

then reconsider f1yb = f1 . (Y "\/" b) as Element of L by A5;

f1yb = (Y "\/" b) "/\" a by A5, A14

.= Y "\/" (b "/\" a) by A1, A12

.= Y by A10, YELLOW_5:8 ;

hence y in rng f1 by A8, A13, FUNCT_1:def 3; :: thesis: verum

A16: for x, y being Element of s1 holds

( x <= y iff f1 . x <= f1 . y )

proof

f1 is V13()
let x, y be Element of s1; :: thesis: ( x <= y iff f1 . x <= f1 . y )

A17: the carrier of s1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;

then x in [#b,(a "\/" b)#] ;

then reconsider X = x as Element of L ;

y in [#b,(a "\/" b)#] by A17;

then reconsider Y = y as Element of L ;

reconsider f1Y = f1 . Y as Element of L by A5;

reconsider f1X = f1 . X as Element of L by A5;

thus ( x <= y implies f1 . x <= f1 . y ) :: thesis: ( f1 . x <= f1 . y implies x <= y )

end;A17: the carrier of s1 = [#b,(a "\/" b)#] by YELLOW_0:def 15;

then x in [#b,(a "\/" b)#] ;

then reconsider X = x as Element of L ;

y in [#b,(a "\/" b)#] by A17;

then reconsider Y = y as Element of L ;

reconsider f1Y = f1 . Y as Element of L by A5;

reconsider f1X = f1 . X as Element of L by A5;

thus ( x <= y implies f1 . x <= f1 . y ) :: thesis: ( f1 . x <= f1 . y implies x <= y )

proof

thus
( f1 . x <= f1 . y implies x <= y )
:: thesis: verum
assume
x <= y
; :: thesis: f1 . x <= f1 . y

then A18: [x,y] in the InternalRel of s1 by ORDERS_2:def 5;

the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13;

then A19: X <= Y by A18, ORDERS_2:def 5;

A20: f1Y = Y "/\" a by A5;

f1X = X "/\" a by A5;

then f1X <= f1Y by A19, A20, WAYBEL_1:1;

hence f1 . x <= f1 . y by YELLOW_0:60; :: thesis: verum

end;then A18: [x,y] in the InternalRel of s1 by ORDERS_2:def 5;

the InternalRel of s1 c= the InternalRel of L by YELLOW_0:def 13;

then A19: X <= Y by A18, ORDERS_2:def 5;

A20: f1Y = Y "/\" a by A5;

f1X = X "/\" a by A5;

then f1X <= f1Y by A19, A20, WAYBEL_1:1;

hence f1 . x <= f1 . y by YELLOW_0:60; :: thesis: verum

proof

assume
f1 . x <= f1 . y
; :: thesis: x <= y

then A21: [(f1 . x),(f1 . y)] in the InternalRel of s2 by ORDERS_2:def 5;

the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13;

then A22: f1X <= f1Y by A21, ORDERS_2:def 5;

A23: f1Y = Y "/\" a by A5;

A24: b <= X by A17, Def4;

f1X = X "/\" a by A5;

then b "\/" (a "/\" X) <= b "\/" (a "/\" Y) by A22, A23, WAYBEL_1:2;

then A25: (b "\/" a) "/\" X <= b "\/" (a "/\" Y) by A1, A24;

A26: X <= b "\/" a by A17, Def4;

b <= Y by A17, Def4;

then (b "\/" a) "/\" X <= (b "\/" a) "/\" Y by A1, A25;

then A27: X <= (b "\/" a) "/\" Y by A26, YELLOW_5:10;

Y <= b "\/" a by A17, Def4;

then X <= Y by A27, YELLOW_5:10;

hence x <= y by YELLOW_0:60; :: thesis: verum

end;then A21: [(f1 . x),(f1 . y)] in the InternalRel of s2 by ORDERS_2:def 5;

the InternalRel of s2 c= the InternalRel of L by YELLOW_0:def 13;

then A22: f1X <= f1Y by A21, ORDERS_2:def 5;

A23: f1Y = Y "/\" a by A5;

A24: b <= X by A17, Def4;

f1X = X "/\" a by A5;

then b "\/" (a "/\" X) <= b "\/" (a "/\" Y) by A22, A23, WAYBEL_1:2;

then A25: (b "\/" a) "/\" X <= b "\/" (a "/\" Y) by A1, A24;

A26: X <= b "\/" a by A17, Def4;

b <= Y by A17, Def4;

then (b "\/" a) "/\" X <= (b "\/" a) "/\" Y by A1, A25;

then A27: X <= (b "\/" a) "/\" Y by A26, YELLOW_5:10;

Y <= b "\/" a by A17, Def4;

then X <= Y by A27, YELLOW_5:10;

hence x <= y by YELLOW_0:60; :: thesis: verum

proof

hence
f is isomorphic
by A15, A16, WAYBEL_0:66; :: thesis: verum
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in K21(f1) or not x2 in K21(f1) or not f1 . x1 = f1 . x2 or x1 = x2 )

assume that

A28: x1 in dom f1 and

A29: x2 in dom f1 and

A30: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2

reconsider X2 = x2 as Element of L by A8, A29;

A31: b <= X2 by A8, A29, Def4;

reconsider X1 = x1 as Element of L by A8, A28;

A32: b <= X1 by A8, A28, Def4;

reconsider f1X1 = f1 . X1 as Element of L by A5, A28;

A33: f1X1 = X1 "/\" a by A5, A28;

reconsider f1X2 = f1 . X2 as Element of L by A5, A29;

A34: f1X2 = X2 "/\" a by A5, A29;

A35: X2 <= a "\/" b by A8, A29, Def4;

X1 <= a "\/" b by A8, A28, Def4;

then X1 = (b "\/" a) "/\" X1 by YELLOW_5:10

.= b "\/" (a "/\" X2) by A1, A30, A32, A33, A34

.= (b "\/" a) "/\" X2 by A1, A31

.= X2 by A35, YELLOW_5:10 ;

hence x1 = x2 ; :: thesis: verum

end;assume that

A28: x1 in dom f1 and

A29: x2 in dom f1 and

A30: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2

reconsider X2 = x2 as Element of L by A8, A29;

A31: b <= X2 by A8, A29, Def4;

reconsider X1 = x1 as Element of L by A8, A28;

A32: b <= X1 by A8, A28, Def4;

reconsider f1X1 = f1 . X1 as Element of L by A5, A28;

A33: f1X1 = X1 "/\" a by A5, A28;

reconsider f1X2 = f1 . X2 as Element of L by A5, A29;

A34: f1X2 = X2 "/\" a by A5, A29;

A35: X2 <= a "\/" b by A8, A29, Def4;

X1 <= a "\/" b by A8, A28, Def4;

then X1 = (b "\/" a) "/\" X1 by YELLOW_5:10

.= b "\/" (a "/\" X2) by A1, A30, A32, A33, A34

.= (b "\/" a) "/\" X2 by A1, A31

.= X2 by A35, YELLOW_5:10 ;

hence x1 = x2 ; :: thesis: verum