let L be non empty RelStr ; :: thesis: for x being Element of L holds

( x in PRIME (L opp) iff x is co-prime )

let x be Element of L; :: thesis: ( x in PRIME (L opp) iff x is co-prime )

then x ~ is prime by WAYBEL_6:def 8;

then x ~ in PRIME (L opp) by WAYBEL_6:def 7;

hence x in PRIME (L opp) by LATTICE3:def 6; :: thesis: verum

( x in PRIME (L opp) iff x is co-prime )

let x be Element of L; :: thesis: ( x in PRIME (L opp) iff x is co-prime )

hereby :: thesis: ( x is co-prime implies x in PRIME (L opp) )

assume
x is co-prime
; :: thesis: x in PRIME (L opp)assume
x in PRIME (L opp)
; :: thesis: x is co-prime

then x ~ in PRIME (L opp) by LATTICE3:def 6;

then x ~ is prime by WAYBEL_6:def 7;

hence x is co-prime by WAYBEL_6:def 8; :: thesis: verum

end;then x ~ in PRIME (L opp) by LATTICE3:def 6;

then x ~ is prime by WAYBEL_6:def 7;

hence x is co-prime by WAYBEL_6:def 8; :: thesis: verum

then x ~ is prime by WAYBEL_6:def 8;

then x ~ in PRIME (L opp) by WAYBEL_6:def 7;

hence x in PRIME (L opp) by LATTICE3:def 6; :: thesis: verum